Re: [isabelle] code generation for saturated naturals

Hi Peter,

>> Well, the first one(s) did not really perform well, but it was not very
>> difficult to get along without it.
> What do you mean by "the first one(s)"? Lemmas, sledgehammers, ... ?

Well, the first metis class was very slow, I did not check the others

>> instantiation sat :: (len) complete_lattice
> You've lost me here - the final instantiation in the theory is precisely this one.

This was a slip, it should read

instantiation sat :: (len) complete_distrib_lattice

which is still left as an exercise to prove.




PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.