[isabelle-dev] typedef (open) legacy
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.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 259 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev