Re: [isabelle] type error
- To: Lawrence Paulson <lp15 at cam.ac.uk>, isabelle-users <isabelle-users at cl.cam.ac.uk>
- Subject: Re: [isabelle] type error
- From: Viorel Preoteasa <viorel.preoteasa at abo.fi>
- Date: Thu, 18 Nov 2010 16:42:25 +0200
- In-reply-to: <D28367C6-EE1E-4086-86AD-2FDDB1A9559F@cam.ac.uk>
- References: <4CE529F2.email@example.com> <D28367C6-EE1E-4086-86AD-2FDDB1A9559F@cam.ac.uk>
- User-agent: Mozilla/5.0 (Windows; U; Windows NT 5.1; en-US; rv:184.108.40.206) Gecko/20101027 Lightning/1.0b2 Thunderbird/3.1.6
On 11/18/2010 4:13 PM, Lawrence Paulson wrote:
The following warning should alert you to the problem:
### Additional type variable(s) in specification of disjunctive: 'd
Thank you for your answer. I have figured it out myself finally. I had this
problem before, but I forgot about it.
Wouldn't be better is Isabelle would give an error already when
defining something which depends on an additional type variable?
For more information, switch on “show types" and you can locate the occurrence of 'd
disjunctive TYPE(?'d) (?R::?'a => ?'b => ?'c) =
(ALL P::?'d => ?'a => ?'b. (?R .. SUP P) = SUP (%w::?'d. ?R .. P w))
An implicit type parameter has been generated in order to ensure that this definition is sound. Probably you should make the right hand side of your definition more specific.
On 18 Nov 2010, at 13:28, Viorel Preoteasa wrote:
I have the following theory. At theorem test I get the following error:
*** Type unification failed: Clash of types "fun" and "bool"
*** Type error in application: Incompatible operand type
*** Operator: Trueprop :: bool => prop
*** Operand: disjunctive (R::??'d::type itself) :: (??'a::type => ??'b::complete_lattice => ??'c::complete_lattice) => bool
*** At command "theorem".
Could someone help me?
imports Main Lattice_Syntax
SUP1_syntax :: "('a => 'b::complete_lattice) => 'b" ("(SUP _)"  1000)
where "SUP P == SUPR UNIV P"
definition apply_fun::"('a=>'b=>'c)=>('a=>'b)=>'a=>'c" (infixl ".." 5) where
"(A .. B) = (% x . (A x) (B x))";
"(disjunctive R) = (! P . (R .. (SUP P)) = (SUP (% w . (R .. (P w)))))";
theorem test: "disjunctive R";
This archive was generated by a fusion of
Pipermail (Mailman edition) and