[isabelle] Referring to type variable of a locale



Hi, I'm running into a problem whose solution should be simple. The following is fine:

class cla = fixes foo :: "'a"
class cla2 = cla + fixes a_set :: "'a set"
begin
lemma lem1: "foo \<in> a_set \<Longrightarrow> true"
sorry
end

Yet what I want is not fine:

locale loc = fixes foo :: "'a"
locale loc2 = loc + fixes a_set :: "'a set"
begin
lemma lem1: "foo \<in> a_set \<Longrightarrow> true"
sorry
end

The error I get is:
Type unification failed
Type error in application: incompatible operand type
Operator: op ∈ foo :: ('b ⇒ bool) ⇒ bool
Operand: a_set :: 'a ⇒ bool

Can I somehow tell Isabelle that I want the type of a_set to be "'a::loc set"?

Thanks in advance for help!





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