Re: [isabelle] Infinite variable chasing

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?

I shall share my finding here as well:

An exception TYPE will be raised: Variable "?stuff" has two distinct
types. I think the problem there is that lookup' checks the type
variables using op = instead, which would match ?'a => ?'b with the
resulting type. I suspect lookup' can't handle schematic types. It'd fail in cases in which Envir.lookup succeeds, e.g.:

g :: "'a => 'b"
a :: real
v :: real

ML {*

val trm1 = @{term_pat "(?f'::(?'a=>?'b)=>?'c) ?stuff = ?v"};

val (_ $ (_ $ var) $ _) = trm1;

val mtch_seq = let
  val init = Envir.empty 0
  val trm2 = @{term "g a = v"}
  Unify.matchers @{theory} [(trm1,trm2)]

val SOME (mtch,_) = nthseq 1711 mtch_seq;

val tenv = Envir.term_env mtch;
val p = Term.dest_Var var;

val inst = Envir.lookup' (tenv, p);


Larry can maybe explain the details behind this...

That'd be great!



The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

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