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
