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 in.tum.de> 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
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 :)
“Syntactic sugar causes cancer of the semi-colons.” 
“Structured Programming supports the law of the excluded muddle.” 
: Epigrams on Programming — Alan J. — P. Yale University
This archive was generated by a fusion of
Pipermail (Mailman edition) and