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
well-defined spots.
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
thread.)
Makarius_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
