# [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.