Re: [isabelle] Changing unification depth



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

Thanks
John



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.