Am Samstag, den 09.01.2016, 17:22 +0100 schrieb Florian Haftmann:
> Ho Johannes.
>
> > > > Then the dictionary construction for type constructors
> > > > does
> > > > not
> > > > work in ML! The type signature would be the following:
> > > >
> > > >val test_prod : ('a * 'b)
Dear all,
there are some changes I would like to add for the upcoming release. It would
be nice, if someone can integrate them:
- improved code equations for binomial coefficients and certain
divmod-algorithms.
(cf.
I already moved a few small lemmas. I also defined the notion of an
algebraic number; as soon as your AFP entry works with the development
version of Isabelle again (is that already the case?), I will prove
equivalence of my definition in Poly_Deriv.thy to your definition in
Algebraic_Numbers
I’m puzzled. In ~~/src/HOL/Library/Poly_Deriv.thy I found no notion of
algebraic number.
Oh, yes, you're right. It's in
https://bitbucket.org/isa-afp/afp-devel/src/363fdbc2f28c2503095a245f00db3d2805ed3ff9/thys/Liouville_Numbers/Liouville_Numbers_Misc.thy
.
Its definitely not optimal, and
Hi Manuel,
> I already moved a few small lemmas.
Thanks.
> I also defined the notion of an algebraic number; as soon as your AFP entry
> works with the development version of Isabelle again (is that already the
> case?),
Yes, it should work. (At least, on Friday afternoon, it worked)
> I
>> I’m puzzled. In ~~/src/HOL/Library/Poly_Deriv.thy I found no notion of
>> algebraic number.
> Oh, yes, you're right. It's in
> https://bitbucket.org/isa-afp/afp-devel/src/363fdbc2f28c2503095a245f00db3d2805ed3ff9/thys/Liouville_Numbers/Liouville_Numbers_Misc.thy
> .
Ah, I see. Indeed:
I have finally installed my great mass of new material, but when I try to test
it, it fails as shown below. I can’t imagine what I could have done to trigger
such an error. Nearly all of my changes are confined to Multivariate_Analysis.
Does anybody have an idea what could be going on here?
I added the efficient code equations for fact and binomial, and similar
ones for pochhammer and gbinomial.
I also adapted everything from Square_Free_Factorization and
Missing_Polynomial that seemed to be of general interest to me
(especially the generalisation of the type of pderiv).
I
It looks like I'm the one who broke it. It does not work after my commit
3201ddb00097, but it still works in Fabian's d8e7738bd2e9 immediately
before.
I have no idea what causes this problem. Maybe one of our resident code
generator experts could comment on it?
I'll try to find out which
On Mon, 11 Jan 2016, Manuel Eberl wrote:
It looks like I'm the one who broke it. It does not work after my commit
3201ddb00097, but it still works in Fabian's d8e7738bd2e9 immediately before.
Just a reminder of the normal routine: push to the Isabelle repository
always requires a full
10 matches
Mail list logo
