Re: [isabelle] type_synonym and fixed type arguments in a locale?
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"
This archive was generated by a fusion of
Pipermail (Mailman edition) and