ADD_CONV : conv

- STRUCTURE
- 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:where s is the numeral that denotes the sum of the natural numbers denoted by m and n.
|- m + n = s

- 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

HOL Kananaskis-14