Re: [isabelle] types and placeholders
Tobias Nipkow wrote:
Your P is polymorphic. Hence two occurrences of P need not have the
same type. Hence Isabelle gave your two P's the most general type, ie
one is of type 'a => bool and the other of type 'b => bool.
Part of the problem is also that the types are also fixed. You can also
specify unknown types, thus
Many problems are typing problems. General advice: always switch on
Isabelle -> Settings -> Show types
when you have a problem.
You can fix it with explicit annotations, eg
theorem "P(x::'a) ==> P(?x21 x :: 'a)"
PS I don't recommend theorems with unknowns in them, but that's a
matter of taste.
"P (x :: 'a) ==> P (?x21 x :: ?'x)" ;
Then also it will work. (Not that there is normally any good reason to
This archive was generated by a fusion of
Pipermail (Mailman edition) and