[Hol-info] EVAL WHILE

[Ramana K. <Ram...@cl...>]

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.