On Wed, 27 Feb 2013, Tobias Nipkow wrote:
All known incidents were of the category as the present one: someone
who is not yet conditioned to watch out for excess polymorphism
stumbles over it, and gets surprised how ond type parameters here
suddenly shows up there. But this can be avoided by
It's absolutely appropriate to send a message to 20 experts rather than 600
users when the latter are very unlikely to have a clue what's going on here.
Anyway, it is a development matter. A behaviour where ... denotes something
other than the previous right-hand side needs to be fixed.
Larry
On Wed, 27 Feb 2013, Lawrence Paulson wrote:
A behaviour where ... denotes something other than the previous
right-hand side needs to be fixed.
Again this odd bug -- fixed terminology. Such problems are much deeper.
Fortunately, the solution for overly polymorphic results, and the extreme
I don't think it's helpful to argue about terminology. Many problems have deep
and complicated causes, as in the case of the Ariane 5 launch failure. They
aren't just simple coding errors, and using the word fixed does not imply
that carelessness is to blame. But I do think that a simple
Am 27/02/2013 15:28, schrieb Makarius:
On Wed, 27 Feb 2013, Lawrence Paulson wrote:
A behaviour where ... denotes something other than the previous right-hand
side needs to be fixed.
Again this odd bug -- fixed terminology. Such problems are much deeper.
Fortunately, the solution for
On Wed, 27 Feb 2013, Lawrence Paulson wrote:
To me it hardly differs from Fails to refine any pending goal, and it
should be treated similarly.
This feature actually has caused a lot of trouble over the years. Just
for Isabelle2013, I had to repair the error-side-exit once again, after it
On Wed, 27 Feb 2013, Tobias Nipkow wrote:
definition my0 :: nat where my0 = length []
into a definition of a constant of type 'a itself ⇒ nat with an
additional parameter. Although this is a legal definition, I never
understood why this is done automatically. The user could also write it
Am 27/02/2013 16:44, schrieb Makarius:
On Wed, 27 Feb 2013, Tobias Nipkow wrote:
definition my0 :: nat where my0 = length []
into a definition of a constant of type 'a itself ⇒ nat with an additional
parameter. Although this is a legal definition, I never understood why this
is
done
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
12 matches
Mail list logo
