Re: [isabelle] type_synonym and fixed type arguments in a locale?
On Tue, 14 May 2013, Randy Pollack wrote:
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"
Witin the locale context type 'a is locally fixed, i.e. a local type
constant. Thus it cannot be used again as parameter for the type_synonym.
You have to avoid the clash of scope manually like this:
type_synonym 'b atm = "int * 'b"
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?
It is in principle possible to support that, but adding even more
infrastructure to local context. The localized version of type_synonym in
Isabelle2013 is still a bit crude in that respect. I did not push this
further so far, because so many other tools that introduce types are not
fully localized yet and need to catch up with the advances from 2009/2010.
This archive was generated by a fusion of
Pipermail (Mailman edition) and