[isabelle-dev] Proposing extensions to the Isabelle library?

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Tue Dec 18 21:18:08 CET 2012

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,


PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 261 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20121218/7bcb5a4a/attachment.sig>

More information about the isabelle-dev mailing list