Evaluation
The evaluation of a rest # S R proceeds as follows. The source
S is evaluated. If the result obtained is an empty ground expression, the
evaluation of the whole construct fails, but, if the result is a failure, the rest
R is evaluated, and the result obtained is taken to be the result of the
whole construct. Thus, this construct enables us to test the "logical negation" of the
condition S.
If the rest R is an empty delimited path (which always returns an empty
ground expression), it may be omitted.
# S =>=> # S ,
Env,0,St |- S => ,St'
---------------------------------
Env,m,St |- # S R => $fail(0),St'
Env,0,St |- S => $fail(k),St'
Env,m,St' |- R => X,St''
-----------------------------
Env,m,St |- # S R => X,St''
Env,0,St |- S => $error(Ge),St'
-----------------------------------
Env,m,St |- # S R => $error(Ge),St'