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)" > oops
The two y's are given separate types. In fact, Isabelle introduces ??'a itself in the process. Tobias > Larry > > Begin forwarded message: > >> From: "W. Li" <[email protected]> >> Subject: A possible bug with Isabelle 2013 >> Date: 26 February 2013 15:56:58 GMT >> To: "L. Paulson" <[email protected]> >> >> lemma "True" >> proof - >> have "True=(∃x. (λ_.True) x)" by simp >> also have "...=(∃x. (λ_.True) x)" >> oops >> >> 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 > [email protected] > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
