Re: [isabelle] Unable to prove easy existential "directly"



I looked through the relevant parts of the Isabelle source code just now
and all I could find was something called "Pattern.trace_unify_fail".
This option seems to be exposed in Proof General through the menu, but
in jEdit, nothing like that seems to exist. There doesn't seem to be a
configuration attribute either, so that one could do something like
"declare [[trace_unify]]".

However, as a workaround, you can do this in jEdit:

ML {*  Pattern.trace_unify_fail := true *}

If you then try an "apply (rule exI)", you get the following error message:

The following types do not unify:
('a ⇒ 'b) ⇒ bool
('c ⇒ 'd) ⇒ bool

Cheers,
Manuel

On 07/19/2013 03:13 PM, Wilmer RICCIOTTI wrote:
> On Friday, July 19, 2013 14:41 CEST, Manuel Eberl <eberlm at in.tum.de> wrote: 
>> Oh my, I must have missed that. Yes, in these cases, it is best to
>> annotate variables in binders. If one does not know where the problem
>> comes from in these cases, it can also be a good idea to enable the
>> unification trace, which shows exactly why a role could not be applied;
>> in this case, probably a clash between the free type variables.
> Now that you mention it, I have been wondering how to enable the 
> unification trace in jEdit...
>
> Best,





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