[isabelle-dev] Datatype alt_names
Alexander Krauss
krauss at in.tum.de
Wed Nov 3 17:04:14 CET 2010
Makarius wrote:
> Grepping through the sources for alt_name right now, I get the
> impression that there was a second motivation: make really sure that the
> synthesized "big_rec_name" variations really work in the target
> context. Due to loss of information in base_name, it could in principle
> clash with other names bound in the same context.
The generated names do use the alt_names component if available, but
this does not really prevent clashes, since empirically, the alt_names
field always contains either NONE or the base names of the types, c.f.
ML {*
Datatype.get_all @{theory}
|> Symtab.dest |> map (apsnd #alt_names)
|> map @{make_string} |> cat_lines |> writeln
*}
So, at least currently, the alternative names are never really different.
Both datatype and rep_datatype seem to offer the possibility to specify
different names here. For rep_datatype this is used once in
Library/Bit.thy, but the name is actually the same. For datatype it
seems to be broken anyway, as reported by Brian.
So it seems that this can be safely eliminated, unless some other
package uses it via the ML interface, which should be easy to check.
Alex
More information about the isabelle-dev
mailing list