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]> 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] > https://lists.sourceforge.net/lists/listinfo/hol-info > >
------------------------------------------------------------------------------
_______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
