Re: [isabelle] What happens to ?thesis when there's a meta-for all quantifier?
On 12.07.2014 00:07, Holden Lee wrote:
> In the example, p and q are of type int==>bool. Contrast:
> lemma "⋀x. (p x)==>(q x)"
> proof -
> term ?thesis (*"q":: "int ⇒ bool"*)
> show ?thesis sorry
> Type unification failed: Clash of types "_ ⇒ _" and "bool"
> Type error in application: incompatible operand type
> Operator: Trueprop :: bool ⇒ prop
> Operand: ?thesis :: int ⇒ bool
If you have a look at ?thesis ("term ?thesis"), you'll see that ?thesis
is a lambda abstraction in this case and must be given a parameter.
This archive was generated by a fusion of
Pipermail (Mailman edition) and