[isabelle] locales and 'types'
This doesn't work as one might hope:
locale X =
fixes a :: "'a"
(* This is fine *)
types 'b Type = "'b set"
(* This should be fine too *)
types 'a Type = "'a set"
*** Locally fixed type arguments "'a" in type declaration "Type"
*** At command "types" ...
Can the implementation be tweaked to account for variable shadowing? I have too many type variables not to use them conventionally...
This archive was generated by a fusion of
Pipermail (Mailman edition) and