[isabelle-dev] Fwd: A possible bug with Isabelle 2013
makarius at sketis.net
Wed Feb 27 16:44:18 CET 2013
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
> explicitly if he really wanted it that way. Chances are he did not. Is
> this functionality actually used in the distribution?
We've had a lot of strange crashes in the past, before it was all unified
towards the implicit introduction of TYPE / itself arguments in a few
There might be other conceptual problems luring, but they did not show up
in the past few years.
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 indicating the spots where polymorphism
happens in the sources in a comprehensive way.
(This implicitly assumes that users are using the Isabelle document model,
not the TTY loop. If this is up to discussion, it should go on another
More information about the isabelle-dev