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
