[isabelle-dev] Fwd: A possible bug with Isabelle 2013
nipkow at in.tum.de
Tue Feb 26 17:27:22 CET 2013
Am 26/02/2013 17:17, schrieb Lawrence Paulson:
> 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.
> lemma "True"
> proof -
> have "True = (∃x. (λy. True) x)" by simp
> also have "... = (∃x. (λy. True) x)"
The two y's are given separate types. In fact, Isabelle introduces ??'a itself
in the process.
> 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
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev