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).


	Makarius





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