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"
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!


--
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.edu
http://pp.info.uni-karlsruhe.de
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.