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
29
30
31
32
33
|
\DOC REAL_RAT_ADD_CONV
\TYPE {REAL_RAT_ADD_CONV : conv}
\SYNOPSIS
Conversion to perform addition on two rational literals of type {:real}.
\DESCRIBE
The call {REAL_RAT_ADD_CONV `c1 + c2`} where {c1} and {c2} are rational
literals of type {:real}, returns {|- c1 + c2 = d} where {d} is the canonical
rational literal that is equal to {c1 + c2}. The literals {c1} and {c2} may
be integer literals ({&n} or {-- &n}), ratios ({&p / &q} or {-- &p / &q}), or
decimals ({#DDD.DDDD} or {#DDD.DDDDeNN}). The result {d} is always put in the
form {&p / &q} or {-- &p / &q} with {q > 1} and {p} and {q} sharing no common
factor, or simply {&p} or {-- &p} when that is impossible.
\FAILURE
Fails if applied to a term that is not the sum of two permitted rational
literals of type {:real}.
\EXAMPLE
{
# REAL_RAT_ADD_CONV `-- &11 / &12 + #0.09`;;
val it : thm = |- -- &11 / &12 + #0.09 = -- &62 / &75
}
\SEEALSO
REAL_RAT_ABS_CONV, REAL_RAT_DIV_CONV, REAL_RAT_EQ_CONV, REAL_RAT_GE_CONV,
REAL_RAT_GT_CONV, REAL_RAT_INV_CONV, REAL_RAT_LE_CONV, REAL_RAT_LT_CONV,
REAL_RAT_MAX_CONV, REAL_RAT_MIN_CONV, REAL_RAT_MUL_CONV, REAL_RAT_NEG_CONV,
REAL_RAT_POW_CONV, REAL_RAT_REDUCE_CONV, REAL_RAT_RED_CONV, REAL_RAT_SUB_CONV.
\ENDDOC
|
