[isabelle-dev] Proposing extensions to the Isabelle library?
florian.haftmann at informatik.tu-muenchen.de
Tue Dec 18 21:18:08 CET 2012
> 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
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: 261 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev