Re: [isabelle] Changing unification depth

On Nov 28, 2010 4:22pm, Makarius <makarius at> wrote:
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, eg,

%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?

Indeed, it was a problem with my context.


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


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