Re: [isabelle] Changing unification depth



> 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.
>

OK. I've tried it with "writeln (Int.toString search_bnd)" instead and
I get a reading of 60 as well, even after I've changed it to 5 with
"declare [[unify_search_bound=5]]". I've looked at some of the
unifiers and they are definitely deeper than 5 levels, e.g.,

%a::nat => nat.
                       a (a (a (a (a (a
 (a (a (a (a (a (a (a (a (a (a (a (a (a
 (a (a (a (a (a (a (a (a (a (a (a (a (a
 (a (a (a (a (a (a (a (a (a (a (a (a (a
 (a (a (a (a (a (a (a (a (a (a (a (a ((h::(nat => bool) => nat)
 (s::nat => bool))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

Thanks

John

>
>        Makarius
>





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