[isabelle-dev] Additional type variable(s) in specification
nipkow at in.tum.de
Thu Dec 2 08:50:42 CET 2010
Is the following behaviour really a good idea and useful?
inductive P :: "nat => bool" where
is accepted but defines
P :: "'a itself => nat => bool"
It does kind of warn me by saying
### Additional type variable(s) in specification of P: 'a
but if you miss that warning, you will be very surprised about the kind
of errors you get later on when using P.
If I give a constant an explicit type, I would prefer Isabelle to
More information about the isabelle-dev