[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 MHonArc.