1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
|
\DOC INT_MUL_CONV
\TYPE {INT_MUL_CONV : conv}
\SYNOPSIS
Conversion to perform multiplication on two integer literals of type {:int}.
\DESCRIBE
The call {INT_MUL_CONV `c1 * c2`} where {c1} and {c2} are integer literals
of type {:int}, returns {|- c1 * c2 = d} where {d} is the canonical integer
literal that is equal to {c1 * c2}. The literals {c1} and {c2} may be of the
form {&n} or {-- &n} (with nonzero {n} in the latter case) and the result will
be of the same form.
\FAILURE
Fails if applied to a term that is not the product of two permitted integer
literals of type {:int}.
\EXAMPLE
{
# INT_MUL_CONV `&6 * -- &9`;;
val it : thm = |- &6 * -- &9 = -- &54
}
\SEEALSO
INT_REDUCE_CONV, REAL_RAT_MUL_CONV.
\ENDDOC
|
