[isabelle-dev] Proposing extensions to the Isabelle library?
coglio at kestrel.edu
Sat Dec 22 04:01:44 CET 2012
Hi Florian, I'd be happy to contribute, so I'll look into that. I don't
have a lot of spare time, so it may take me a while. The Jan or Feb
release is "safe" :)
On 12/18/12 12:18 PM, Florian Haftmann wrote:
> Hi Alessandro,
>> Is there any plan to make things in the library more uniform (one way or
>> the other)? Is there a preference for new type classes should be
>> developed (purely syntactic or with assumptions)?
> well, there is no big masterplan. Usually things evolve: somebody
> thinks about an extended or more fine-grained hierarchy and thinks how
> to accomplish things without breaking more than necessary.
>> Personally, I like syntactic classes because they are more modular. For
>> example, in the library extensions that I sent the other day, the
>> definition of type class finite_lattice_complete would be perhaps
>> slightly cleaner if bot and top were syntactic classes like Inf and Sup.
>> Just my 2 cents.
> I.e. something like
> class bot ~> class order_bot
> class top ~> class order_top
> class bot = fixes bot :: "'a"
> class top = fixes top :: "'a"
> Could make sense. The question is whether somebody is willing to
> undertake this change. If you would consider this, you find the first
> clues at
> Get back here if questions remain.
> Note that currently we are heading towards a next release in January or
> February, and time might be too terse to polish and incorporate a change
> like the one sketched above.
> Hope this helps,
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 3735 bytes
Desc: S/MIME Cryptographic Signature
More information about the isabelle-dev