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

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!

Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Geb. 50.41, Raum 031
76131 Karlsruhe

Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft

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