Interesting! So it's not a problem with the compset at whileTheory in the default build, but something further down the line...
I can confirm that in my very late context, explicitly specifying naturals stops the loop, so the problem is something to do with integers. Thanks Yong Kiam and Michael. On 13 October 2015 at 15:30, Michael Norrish <michael.norr...@nicta.com.au> wrote: > 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 <tanyongk...@gmail.com> 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 <ramana.ku...@cl.cam.ac.uk> > 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 >> hol-info@lists.sourceforge.net >> https://lists.sourceforge.net/lists/listinfo/hol-info >> >> > > ------------------------------------------------------------------------------ > _______________________________________________ > hol-info mailing list > hol-info@lists.sourceforge.net > 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 > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info > >
------------------------------------------------------------------------------
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
