MUL_CONV : conv

- STRUCTURE
- SYNOPSIS
- Calculates by inference the product of two numerals.
- LIBRARY
- reduce
- DESCRIPTION
- If m and n are numerals (e.g. 0, 1, 2, 3,...), then MUL_CONV "m * n" returns the theorem:where s is the numeral that denotes the product of the natural numbers denoted by m and n.
|- m * n = s

- FAILURE
- MUL_CONV tm fails unless tm is of the form "m * n", where m and n are numerals.
- EXAMPLE
#MUL_CONV "0 * 12";; |- 0 * 12 = 0 #MUL_CONV "1 * 1";; |- 1 * 1 = 1 #MUL_CONV "6 * 11";; |- 6 * 11 = 66

HOL Kananaskis-14