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