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
,...), 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.
EXAMPLE
#ADD_CONV "75 + 25";; |- 75 + 25 = 100
HOL
Kananaskis-8