Re: [isabelle] Changing unification depth



On Sat, 27 Nov 2010, munddr at gmail.com wrote:

Here's how ref is assigned:

fun hounifiers (thy,env, tus : (term*term)list)

: (Envir.env * (term*term)list)Seq.seq =

let

...

in (ref := search_bnd; add_unify 1 ((env, dps), Seq.empty)) end;


Just a follow-up question: If unify_search_bound is updated, I should expect to see ref to be updated there, right?

Hard to say from this tiny extract of the source above. There could be some unexpected effects due to lazy evaluation or parallelism. Mutable references are a source of many problems and being gradually removed from the system.

For experimentation, it is usually easier to print out something using writeln or similar.


	Makarius





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