Re: [isabelle] Hide all constructors of a datatype automatically


May a solution can be found somewhere in “implementation.pdf”, from the documentation pan. I believe it's possible to modify a theory context using an embedded SML function (embedded in the theory file), without a need for modifying Isabelle internal (I'm looking at it, will be back if I feel I've found anything useful in “implementation.pdf”).

Le Sat, 14 Dec 2013 12:50:09 +0100, René Neumann <rene.neumann at> a écrit:


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é

“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

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