# [isabelle] type error

*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>
*Subject*: [isabelle] type error
*From*: Viorel Preoteasa <viorel.preoteasa at abo.fi>
*Date*: Thu, 18 Nov 2010 15:28:18 +0200
*User-agent*: Mozilla/5.0 (Windows; U; Windows NT 5.1; en-US; rv:1.9.2.12) Gecko/20101027 Lightning/1.0b2 Thunderbird/3.1.6

Hello,
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?
Best regards,
Viorel
theory Test
imports Main Lattice_Syntax
begin
abbreviation

` SUP1_syntax :: "('a => 'b::complete_lattice) => 'b" ("(SUP _)"
``[1000] 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))";
definition

` "(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
MHonArc.*