[isabelle] Syntax translation for types
I would like to have Isabelle print types using the type abbreviations I
have introduced with "types". To that end, I have come across
translations for types that work reasonably well if type variables occur
only once. However, I fail to make it work for type abbreviation like this:
types 'a my_type = "('a list × int × 'a list)"
"my_type a" <= (type) "a list × int × a list"
Isabelle complains that variable a occurs twice in "a list × int × a
list". How can I set up an appropriate print translation for such a type
abbreviation? Do I need to write an ML translation function? If so, how
can I find out how to do that? Or is there any better support other than
translations (similar to abbreviation for constants)?
This archive was generated by a fusion of
Pipermail (Mailman edition) and