[isabelle] type_synonym and fixed type arguments in a locale?
Consider the cut-down locale definition:
locale step =
label:lattice where sup = lblsup
for lblsup::"'a => 'a => 'a"
In the context of this locale want a type synonym:
type_synonym 'a atm = "int * 'a"
This is rejected:
*** Locally fixed type arguments "'a" in type declaration "atm"
OK, but the following is also rejected:
type_synonym atm = "int * 'a"
*** Extra variables on rhs: "'a"
Is it possible to make such a type synonym in a locale?
This archive was generated by a fusion of
Pipermail (Mailman edition) and