Re: [isabelle] THE - equality
You need a type constraint:
lemma "(THE x::int. x + 1 = 3) = 2"
Otherwise, Isabelle doesn’t know what sort of numbers you are talking about. Numerals are polymorphic.
On 18 Apr 2014, at 11:24, Roger H. <s57076 at hotmail.com> wrote:
> how can i prove
> (THE x. x + 1 = 3) = 2 ?
> "apply (rule the_equality, simp)"
> i get:
> ⋀x. x + 1 = 3 ⟹ x = 2
> I think i have to prove that the solution is unique.
> how do i continue?
> Thank you!
This archive was generated by a fusion of
Pipermail (Mailman edition) and