INT_RED_CONV : term -> thm

SYNOPSIS
Performs one arithmetic or relational operation on integer literals of type :int.

DESCRIPTION
When applied to any of the terms `--c`, `abs c`, `c1 + c2`, `c1 - c2`, `c1 * c2`, `c pow n`, `c1 <= c2`, `c1 < c2`, `c1 >= c2`, `c1 > c2`, `c1 = c2`, where c, c1 and c2 are integer literals of type :int and n is a numeral of type :num, INT_RED_CONV returns a theorem asserting the equivalence of the term to a canonical integer (for the arithmetic operators) or a truth-value (for the relational operators). The integer literals are terms of the form &n or -- &n (with nonzero n in the latter case).

FAILURE CONDITIONS
Fails if applied to an inappropriate term.

USES
More convenient for most purposes is INT_REDUCE_CONV, which applies these evaluation conversions recursively at depth, or still more generally REAL_RAT_REDUCE_CONV which applies to any rational numbers, not just integers. Still, access to this `one-step' reduction can be handy if you want to add a conversion conv for some other operator on int number literals, which you can conveniently incorporate it into INT_REDUCE_CONV with
  # let INT_REDUCE_CONV' =
      DEPTH_CONV(INT_RED_CONV ORELSEC conv);;

SEE ALSO
INT_REDUCE_CONV, REAL_RAT_RED_CONV.