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 =
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
For experimentation, it is usually easier to print out something using
writeln or similar.
This archive was generated by a fusion of
Pipermail (Mailman edition) and