REDUCE_CONV : conv
STRUCTURE
numLib
SYNOPSIS
Evaluate ground expressions involving arithemetic and boolean operations.
DESCRIPTION
An invocation REDUCE_CONV M, where M is a ground term made up of the standard boolean and numerical operators, uses deductive steps to perform any possible reductions, yielding the result N. The theorem |- M = N is returned.
FAILURE
Never fails.
EXAMPLE
- REDUCE_CONV (Term `!x:num. x = x`);
> val it = |- (!x. x = x) = !x. T : thm

- REDUCE_CONV
    (Term`(y = (((2 + 4 - 1) * 5) ** 3) DIV 2) /\ (p \/ T ==> q)`);
> val it =
    |- (y = ((2 + 4 - 1) * 5) ** 3 DIV 2) /\ (p \/ T ==> q) =
       (y = 7812) /\ q : thm
SEEALSO
EVAL
HOL  Kananaskis-13