Re: [isabelle] datatype display problem of type_synonym
On Tue, 17 Jul 2012, Ramana Kumar wrote:
On Tue, Jul 17, 2012 at 8:22 AM, Tobias Nipkow <nipkow at in.tum.de> wrote:
Type synonyms are expanded during parsing. They beautify the input but
cannot occur in the output.
In HOL4, the printer attempts to use user-defined type synonyms when
possible, helping increase consistency between input and output.
Sometimes, of course, if you have many synonyms for the same type, you
get the wrong one printed.
Was it a principled decision not to print synonyms in Isabelle?
The question of reverting type synonyms pops up every couple of years, and
I have reconsidered it myself many times already. There have been
counter-indications both from users getting confused about arbitrary
type-subexpressions being subject to contraction, and technical problems
in the interaction with other syntax mechanisms (such as translations that
may depend on type information).
So Isabelle does not support that, and probably never will support it.
Nonetheless, some libraries try to simulate it via 'translations' for the
ASTs stemming from types, but this causes other surprises (as I've just
seen again in the output of 'print_theory' yesterday).
This archive was generated by a fusion of
Pipermail (Mailman edition) and