Email Gateway (Aug 18 2022 at 18:56): Email Gateway (Aug 18 2022 at 18:56):From: Stephan van Staden <Stephan.vanStaden@inf.ethz.ch>
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!
Email Gateway (Aug 18 2022 at 18:56):From: Peter Gammie <peteg42@gmail.com>
Stephan,
You can use a "for" clause to constrain the type of foo:
locale loc = fixes foo :: "'a"
locale loc2 = loc foo for foo :: "'a" + fixes a_set :: "'a set"
begin
lemma lem1: "foo \<in> a_set \<Longrightarrow> true"
sorry
end
There is a lot of information in the mailing list archives about locales - hopefully you can find it without too much bother.
cheers
peter
Email Gateway (Aug 18 2022 at 18:56):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
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
Email Gateway (Aug 18 2022 at 18:56):From: Stephan van Staden <Stephan.vanStaden@inf.ethz.ch>
Thanks for the help, Peter and Andreas. Problem solved! :)
Stephan
Last updated: Apr 26 2024 at 20:16 UTC