ADD_CONV : conv
STRUCTURE
reduceLib
SYNOPSIS
Calculates by inference the sum of two numerals.
LIBRARY
reduce
DESCRIPTION
If
m
and
n
are numerals (e.g.
0
,
1
,
2
,
3
,...) of type
:num
, then
ADD_CONV ``m + n``
returns the theorem:
|- m + n = s
where
s
is the numeral that denotes the sum of the natural numbers denoted by
m
and
n
.
FAILURE
ADD_CONV tm
fails unless
tm
is of the form
``m + n``
, where
m
and
n
are numerals of type
:num
.
EXAMPLE
> ADD_CONV ``75 + 25``; val it = |- 75 + 25 = 100 : thm
SEEALSO
MUL_CONV
HOL
Kananaskis-13