[isabelle-dev] Fwd: A possible bug with Isabelle 2013
lp15 at cam.ac.uk
Tue Feb 26 17:17:52 CET 2013
A student has forwarded this problem to me. It seems weird and unbelievable. What have I overlooked?
I tidied it up slightly (see below) but I get the same error message.
have "True = (∃x. (λy. True) x)" by simp
also have "... = (∃x. (λy. True) x)"
Begin forwarded message:
> From: "W. Li" <wl302 at cam.ac.uk>
> Subject: A possible bug with Isabelle 2013
> Date: 26 February 2013 15:56:58 GMT
> To: "L. Paulson" <lp15 at cam.ac.uk>
> lemma "True"
> proof -
> have "True=(∃x. (λ_.True) x)" by simp
> also have "...=(∃x. (λ_.True) x)"
> Here is the error message:
> Type unification failed: Clash of types "bool" and "_ ⇒ _"
> Type error in application: incompatible operand type
> Operator: op = … :: (??'a itself ⇒ bool) ⇒ bool
> Operand: ∃x. True :: bool
More information about the isabelle-dev