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.

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)"

Tobias

PS I don't recommend theorems with unknowns in them, but that's a matter of taste.
Part of the problem is also that the types are also fixed. You can also specify unknown types, thus

"P (x :: 'a) ==> P (?x21 x :: ?'x)" ;

Then also it will work. (Not that there is normally any good reason to do this)

Jeremy






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.