Re: [isabelle] Changing unification depth



On Sun, 28 Nov 2010, John Munroe wrote:

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

That's very strange. Are you sure you have the correct context in your example? One where the "declare [[unify_search_bound=5]]" is effective?

Can you show a self-contained snippet of theory source text?


	Makarius





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