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

[Alessandro Coglio]

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


-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 3735 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20121221/613fc9de/attachment.bin>