> 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.
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
