RESTR_EVAL_CONV : term list -> conv
STRUCTURE
SYNOPSIS
Symbolically evaluate a term, except for specified constants.
DESCRIPTION
An application RESTR_EVAL_CONV [c1, ..., cn] M evaluates the term M in the call-by-value style of EVAL. When a type instance c of any element in c1,...,cn is encountered, c is not expanded by RESTR_EVAL_CONV. The effect is that evaluation stops at c (even though any arguments to c may be evaluated). This facility can be used to control EVAL_CONV to some extent.
FAILURE
Never fails, but may diverge.
EXAMPLE
In the following, we first attempt to map the factorial function FACT over a list of variables. This attempt goes into a loop, because the conditional statement in the evaluation rule for FACT is never determine when the argument is equal to zero. However, if we suppress the evaluation of FACT, then we can return a useful answer.
   - EVAL (Term `MAP FACT [x; y; z]`);   (* loops! *)
   > Interrupted.

   - val [FACT] = decls "FACT";   (* find FACT constant *)
   > val FACT = `FACT` : term

   - RESTR_EVAL_CONV [FACT] (Term `MAP FACT [x; y; z]`);

   > val it = |- MAP FACT [x; y; z] = [FACT x; FACT y; FACT z] : thm
USES
Controlling symbolic evaluation when it loops or becomes exponential.
SEEALSO
HOL  Kananaskis-13