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.
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";
<>
val it = (): unit
> show_types := true;
val it = (): unit
> EVAL ``WHILE (\x. x = 0) (\x. x) 1``;
<>
val it =
|- WHILE
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
wrote:
> To my surprise, EVAL went into a loop on the following term:
> ``WHILE (\x. x = 0) (\x. x) 1
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 whic
