----------------------------------------------------------------------
EVAL                                                         (bossLib)
----------------------------------------------------------------------
EVAL : conv

SYNOPSIS
Evaluate a term by deduction.

KEYWORDS
evaluation.

DESCRIBE
An invocation {EVAL M} symbolically evaluates {M} by applying the defining
equations of constants occurring in {M}. These equations are held
in a mutable datastructure that is automatically added to
by {Hol_datatype}, {Define}, and {tprove}. The underlying
algorithm is call-by-value with a few differences, see the entry for
{CBV_CONV} for details.



FAILURE
Never fails, but may diverge.

EXAMPLE

- EVAL (Term `REVERSE (MAP (\x. x + a) [x;y;z])`);
> val it = |- REVERSE (MAP (\x. x + a) [x; y; z]) = [z + a; y + a; x + a]
   : thm


COMMENTS
In order for recursive functions over numbers to be applied by {EVAL},
pattern matching over {SUC} and {0} needs to be replaced by destructors.
For example, the equations for {FACT} would have to be rephrased
as {FACT n = if n = 0 then 1 else n * FACT (n-1)}.

SEEALSO
computeLib.CBV_CONV, computeLib.RESTR_EVAL_CONV, bossLib.EVAL_TAC,
computeLib.monitoring, bossLib.Define.

----------------------------------------------------------------------