# Unclear TLC evaluation behavior

While writing a specification I came across a TLC evaluation strategy that isn't clear to me. I've reproduced it in the following trivial (and nonsensical) spec:

VARIABLE x, a

vars == <<x, a>>

TypeOK == /\ x \in Nat

/\ a \in BOOLEAN

Init == x = 1 /\ a = TRUE

Sub == x' = x + 1

Next == (omitted)

Spec == Init /\ [][Next]_vars

When I define Next as

Next ==

IF Sub THEN

a' = ~a

ELSE

UNCHANGED a

and run TLC, I get the error "In evaluation, the identifier x is either undefined or not an operator", which points to the x' token of Sub. The same happens when I define next as

Next ==

Sub => a' = ~a

When I define Next to be

Next ==

LET p == Sub IN

a' = ~a

I get the error "Successor state is not completely specified by the next-state action" (this could perhaps be explained by lazy evaluation).

Reading about TLC's evaluation rules in chapter 14 of "the book", I couldn't find something that would explain this behavior. Does TLC only evaluate primed assignments when written as simple conjuncts or disjuncts?

Ron