[isabelle] Hide all constructors of a datatype automatically


for modelling an AST I got lots of datatypes together with their
constructors (about 100). As the types and the constructors have rather
generic names, I only want them to be accessed with a prefix. Normally I
would use hide_const and hide_type for this, but explicitly writing all
of the 100 constructors again seems cumbersome and error-prone.

Is there some generic mechanism for declaring them and NOT putting the
names into the global namespace?

A workaround I found is using datatype_new inside a locale, in the
following manner

locale ast

datatype_new binOp = …
datatype_new expr = …

interpretation AST!: ast .

(* register them all again for code-generation *)
datatype_new_compat AST.binOP AST.expr …

But it still feels somewhat wrong for me. Especially throwing two
different datatype packages at it just for hiding names :)

- René
René Neumann

Institut für Informatik (I7)
Technische Universität München
Boltzmannstr. 3
85748 Garching b. München

Tel: +49-89-289-17232
Office: MI 03.11.055

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.