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
Larry
Begin
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
That mysterious type always throws me.
I guess you are saying that this dangling type dependence introduces a function
type in the first line. Unfortunately, this is a difficult matter to explain to
a student. I'll just have to tell him to constrain the types of his bound
variables. I believe
Am 26/02/2013 17:37, schrieb Lawrence Paulson:
That mysterious type always throws me.
I guess you are saying that this dangling type dependence introduces a
function type in the first line. Unfortunately, this is a difficult matter to
explain to a student.
I agree. I have yet to see a
