Re: [isabelle] Infinite variable chasing
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