[isabelle-dev] typedef (open) legacy

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Thu Oct 4 19:01:42 CEST 2012

> I think either option 3 or 4 would make sense, although I'd say 4 is
> preferable for a couple of reasons: First, it makes the implementation
> of typedef simpler. Second, it actually gives users more flexibility
> because if they want a set constant, they can use any definition
> package, not just "definition". The extra verbosity in some cases is a
> small price to pay.

I would support (4).  In the long run, typedef should be the bare
foundational minimum for introducing HOL types, whereas all user-level
features could go to a command type_definition with support for the
quotient package, reasonable user-level rules, code generator setup etc.



PGP available:

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

More information about the isabelle-dev mailing list