Re: [isabelle] type_synonym and fixed type arguments in a locale?



Hi Randy,

Am 14.05.2013 um 23:48 schrieb Randy Pollack <rpollack at inf.ed.ac.uk>:

> 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"

The above looks like a bug. However, there's an easy workaround:

    type_synonym 'b atm = "int * 'b"

Cheers,

Jasmin





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.