[isabelle] locales and 'types'



Hello,

This doesn't work as one might hope:

theory t
imports Main
begin

locale X =
  fixes a :: "'a"
begin

(* 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...

cheers
peter

-- 
http://peteg.org/






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