RESTR_EVAL_TAC
computeLib.RESTR_EVAL_TAC : term list -> tactic
Symbolically evaluate a theorem, except for specified constants.
This is a tactic version of RESTR_EVAL_CONV.
Failure
As for RESTR_EVAL_CONV.
Controlling symbolic evaluation when it loops or becomes exponential.
See also
bossLib.EVAL,
bossLib.EVAL_RULE,
bossLib.EVAL_TAC,
computeLib.RESTR_EVAL_CONV,
computeLib.RESTR_EVAL_RULE