Re: [isabelle] Infinite variable chasing

Hi Michael,

I'm having a problem with looking up the instantiation to a variable in a matcher with Envir.lookup.

I just looked at the code in envir.ML again, and there is a function lookup', preceded by the following comment:

(* When dealing with environments produced by matching instead *)
(* of unification, there is no need to chase assigned TVars.   *)
(* In this case, we can simply ignore the type substitution    *)
(* and use = instead of eq_type.                               *)

Could this be the source of your problem? Since your problematic substitution is generated by Unify.matchers (which wasn't clear from you question), have you tried lookup' instead of lookup?

Larry can maybe explain the details behind this...


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