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

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


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"

Alternatively, you can redeclare foo explicitly:

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

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,

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

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

Yet what I want is not fine:

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

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.