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

[Florian Haftmann]

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
http://isabelle.in.tum.de/repos/isabelle/file/c5e0073558f3/README_REPOSITORY.
 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,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- 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>