I just tried it with integers and naturals and both worked: > EVAL ``WHILE (\x. x = 0n) (\x. x) 1``; val it = |- WHILE (λx. x = 0) (λx. x) 1 = 1: thm > load "intLib"; <<HOL message: intLib loaded. Use intLib.deprecate_int() to turn off integer parsing>> val it = (): unit > show_types := true; val it = (): unit > EVAL ``WHILE (\x. x = 0) (\x. x) 1``; <<HOL message: more than one resolution of overloading was possible>> val it = |- WHILE (λ(x :int). x = (0 :int)) (λ(x :int). x) (1 :int) = (1 :int): thm
This was at 631a4e105ed0 Michael On 13 Oct 2015, at 14:57, Yong Kiam <[email protected]<mailto:[email protected]>> wrote: I tried it and got the same problem BUT it only occurred after I opened integerTheory. Additionally, ``WHILE (\x.x=(0:num)) (\x.x) 1`` evals fine. On Tue, Oct 13, 2015 at 11:11 AM, Ramana Kumar <[email protected]<mailto:[email protected]>> wrote: To my surprise, EVAL went into a loop on the following term: ``WHILE (\x. x = 0) (\x. x) 1`` I thought in the default setup, EVAL would only evaluate the first argument of a conditional, reducing it to true or false, skipping the other arguments (the then and else branches) until it was known which one to follow. Now, even if that is not the default behaviour of EVAL, I can't even figure out how to set up a compset to get that behaviour. Does anyone know how? The default setup uses lazyfy_thm on COND_CLAUSES, with a set_skip of NONE, which I would have thought would be right, but it goes into a loop on the above term. ------------------------------------------------------------------------------ _______________________________________________ hol-info mailing list [email protected]<mailto:[email protected]> https://lists.sourceforge.net/lists/listinfo/hol-info ------------------------------------------------------------------------------ _______________________________________________ hol-info mailing list [email protected]<mailto:[email protected]> https://lists.sourceforge.net/lists/listinfo/hol-info ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
------------------------------------------------------------------------------
_______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
