Re: [isabelle] Referring to type variable of a locale



Thanks for the help, Peter and Andreas. Problem solved! :)

Stephan


On 01/17/2012 09:22 AM, Andreas Lochbihler wrote:
Hi Stephan,

You can constrain foo's type to 'a in loc2 as follows:

locale loc2 = loc +
  fixes a_set :: "'a set"
  constrains foo :: "'a"
begin

Alternatively, you can redeclare foo explicitly:

locale loc2 = loc foo
  for foo :: "'a" +
  fixes a_set :: "'a set"
begin

The second solution would erase all mixfix syntax for foo if there was any.

Since type classes must mention exactly one type type variable, so Isabelle unifies the type variables, but locales do not have this restriction.

Hope this helps,
Andreas

Am 16.01.2012 14:57, schrieb Stephan van Staden:
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.