##### 1.4.5Rational and Complex Arithmetic

 (* num ...)
Multiplies the given numbers together, taking any number of arguments. This is a macro that expands into calls of the function binary-*

Examples:

 > (*) 1 > (* 2) 2 > (* 1 2 3) 6

 (+ num ...)
Adds the given numbers together, taking any number of arguments. This is a macro that expands into calls of the function binary-+.

Examples:

 > (+) 0 > (+ 2) 2 > (+ 1 2 3) 6

 (- num num)
Subtracts the given numbers. If only one argument is given, returns the negation of the input.

Examples:

 > (- 5) -5 > (- 5 3) 2

 (/ num num)
Divides the first number by the second. If only one argument is given, returns the reciprocal of the input.

Examples:

 > (/ 2) 1/2 > (/ 16 4) 4

 (1+ num)
Adds 1 to the given number.

Example:

 > (1+ 1) 2

 (1- num)
Subtracts 1 from the given number.

Example:

 > (1- 1) 0

 (binary-* x y) → t x : (acl2-numberp x) y : (acl2-numberp y)
Takes exactly two numbers and multiplies them together.

Example:

 > (binary-* 9 8) 72

 (binary-+ x y) → t x : (acl2-numberp x) y : (acl2-numberp y)
Takes exactly two numbers and adds them together.

Example:

 > (binary-+ 9 8) 17

 (/= x y) → t x : (acl2-numberp x) y : (acl2-numberp y)
Determines if the given numbers are not equal. Logically equivalent to (not (equal x y))

Examples:

 > (/= 2 2) '() > (/= 3 2) 't

 (< x y) → t x : (rationalp x) y : (rationalp y)
Determines if x is less than y.

Examples:

 > (< 1 2) 't > (< 2 1) '() > (< 2 2) '()

 (<= x y) → t x : (rationalp x) y : (rationalp y)
Determines if x is less than or equal to y.

Examples:

 > (<= 1 2) 't > (<= 2 1) '() > (<= 2 2) 't

 (= x y) → t x : (acl2-numberp x) y : (acl2-numberp y)
Determines if x is equal to y. This is like equal, but has the guard that both of its arguments must be numbers. It usually executes more efficiently thatn equal.

Examples:

 > (= 1 2) '() > (= 2 1) '() > (= 2 2) 't

 (> x y) → t x : (rationalp x) y : (rationalp y)
Determines if x is greater than y.

Examples:

 > (> 1 2) '() > (> 2 1) 't > (> 2 2) '()

 (>= x y) → t x : (rationalp x) y : (rationalp y)
Determines if x is greater than or equal to y.

Examples:

 > (>= 1 2) '() > (>= 2 1) 't > (>= 2 2) 't

 (acl2-numberp x)
Returns true if and only if x is a rational or complex rational number.

Examples:

 > (acl2-numberp 1) 't > (acl2-numberp 12/5) 't > (acl2-numberp "no") '()

 (complex-rationalp z)
Determines if z is a complex number consisting of rational parts.

Examples:

 > (complex-rationalp 3) '() > (complex-rationalp (complex 3 0)) '() > (complex-rationalp t) '() > (complex-rationalp (complex 3 1)) 't

 (complex/complex-rationalp z) → t z : t
For most cases, this is simply a macro abbreviating complex-rationalp.

Examples:

 > (complex/complex-rationalp 3) '() > (complex/complex-rationalp (complex 3 0)) '() > (complex/complex-rationalp t) '() > (complex/complex-rationalp (complex 3 1)) 't

 (zp v) → t v : natp
This is a test for the base case (zero) of recursion on the natural numbers.

Examples:

 > :eval reference to undefined identifier: :eval > the-evaluator reference to undefined identifier: the-evaluator > (zp 0) reference to undefined identifier: zp > (zp 1) reference to undefined identifier: zp

 (minusp x) → t x : (real/rationalp x)
Determines whether x is a negative number.

Examples:

 > (minusp 1) '() > (minusp -1) 't

 (natp x) → t x : t
Determines if x is a natural number.

Examples:

 > (natp 1) 't > (natp 0) 't > (natp -1) '()

 (oddp x) → t x : (integerp x)
Determines if x is odd.

Examples:

 > (oddp 3) 't > (oddp 2) '()

 (plusp x) → t x : (real/rationalp x)
Determines if x is positive.

Examples:

 > (plusp 1) 't > (plusp -1) '() > (plusp 1/2) 't

 (posp x) → t x : t
Determines if x is a positive integer.

Examples:

 > (posp 1) 't > (posp -1) '() > (posp 1/2) '() > (posp (complex 1 2)) '() > (posp "asdf") '()

 (rationalp x)
Determines if x is a rational number.

Examples:

 > (rationalp 2/5) 't > (rationalp 2) 't > (rationalp (complex 1 2)) '() > (rationalp "number") '()

 (real/rationalp x)
In most cases, this is just a macro abbreviating rationalp.

Examples:

 > (real/rationalp 2/5) 't > (real/rationalp "number") '()

 (abs x) → t x : (real/rationalp x)
Computes the absolute value of x.

Examples:

 > (abs 1) 1 > (abs -1) 1

 (ceiling i j) → t i : (real/rationalp i) j : (and (real/rationalp j) (not (eql j 0)))
Returns the smallest integer greater the value of (/ i j).

Examples:

 > (ceiling 4 2) 2 > (ceiling 4 3) 2

 (complex n i) → t n : (rationalp n) i : (rationalp i)
Creates a complex number with real part n and imaginary part i.

Examples:

 > (complex 2 1) 2+1i > (complex 2 0) 2 > (complex 0 2) 0+2i > (complex 1/2 3/2) 1/2+3/2i

 (conjugate x) → t x : (acl2-numberp x)
Computes the complex conjugate of x (the result of negating its imaginary part).

Example:

 > (conjugate (complex 3 1)) 3-1i

 (denominator x) → t x : (rationalp x)
Returns the divisor of a rational number in lowest terms.

Examples:

 > (denominator 5) 1 > (denominator 5/3) 3 > (denominator 5/3) 3

 (evenp x) → t x : (integerp x)
Determines if x is even.

Examples:

 > (evenp 1) '() > (evenp 2) 't

 (explode-nonnegative-integer n r) → l n : (and (integerp n) (>= n 0)) r : (print-base-p r)
Returns a list of characters representing n in base-r, and appends l to the end.

Examples:

 > (explode-nonnegative-integer 925 10 nil) '(#\9 #\2 #\5) > (explode-nonnegative-integer 325 16 nil) '(#\1 #\4 #\5) > (explode-nonnegative-integer 325 16 (list 'a 'b 'c)) '(#\1 #\4 #\5 a b c) > (explode-nonnegative-integer 325 16 'a) '(#\1 #\4 #\5 . a)

 (expt i j) → t i : (acl2-numberp i) j : (and (integerp j) (not (and (eql i 0) (< j 0))))
Raises i to the jth power.

Examples:

 > (expt 10 2) 100 > (expt 10 -2) 1/100

 (fix x) → t x : t
Coerces x to a number. If x is a number, (fix x) returns the argument unchanged. Otherwise, it returns 0.

Examples:

 > (fix 20) 20 > (fix 2/3) 2/3 > (fix "hello") 0 > (fix nil) 0

 (floor i j) → t i : (real/rationalp i) j : (and (real/rationalp j) (not (eql j 0)))
Returns the greatest integer not exceeding the value of (/ i j).

Examples:

 > (floor 4 2) 2 > (floor 4 3) 1

 (ifix x) → t x : t
Coerces x to an integer. If x is an integer, (ifix x) returns the argument unchanged. Otherwise, it returns 0.

Examples:

 > (ifix 16) 16 > (ifix 22/3) 0 > (ifix "hello") 0

 (imagpart i) → t i : (acl2-numberp i)
Returns the imaginary part of a complex number.

Examples:

 > (imagpart (complex 3 2)) 2 > (imagpart 5) 0

 (int= i j)
Checks to see if the two integers i and j are equal. This is like equal and =, but with the added guard that the inputs are integers. This generally executes more efficiently on integers than equal or =.

Examples:

 > (int= 1 2) '() > (int= 2 1) '() > (int= 2 2) 't

 (integer-length x) → t x : (integerp x)
Returns the number of bits in the two’s complement binary representation of x.

Examples:

 > (integer-length 12) 4 > (integer-length 1234) 11

 (integerp x)
Determines whether x is an integer.

Examples:

 > (integerp 12) 't > (integerp '12) 't > (integerp nil) '()

 (max i j) → t i : (real/rationalp i) j : (real/rationalp j)
Returns the greater of the two given numbers.

Examples:

 > (max 1 2) 2 > (max 4 3) 4

 (min i j) → t i : (real/rationalp i) j : (real/rationalp j)
Returns the lesser of the two given numbers.

Examples:

 > (min 1 2) 1 > (min 4 3) 3

 (mod i j) → t i : (real/rationalp i) j : (and (real/rationalp j) (not (eql j 0)))
Computes the remainder of dividing i by j.

Examples:

 > (mod 4 2) 0 > (mod 8 3) 2

 (nfix x) → t x : t
Coerces x to a natural number. If x is a natural number, (nfix x) returns the argument unchanged. Otherwise, it returns 0.

Examples:

 > (nfix 1) 1 > (nfix -1) 0 > (nfix 1/2) 0 > (nfix "5") 0

 (nonnegative-integer-quotient x y) → t x : (and (integerp x) (not (< x 0))) y : (and (integerp j) (< 0 j))
Returns the integer quotient of x and y. That is, (nonnegative-integer-quotient x y) is the largest integer k such that (* j k) is less than or equal to x.

Examples:

 > (nonnegative-integer-quotient 14 3) 4 > (nonnegative-integer-quotient 15 3) 5

 (numerator x) → t x : (rationalp x)
Returns the dividend of a rational number in lowest terms.

Examples:

 > (numerator 4) 4 > (numerator 6/7) 6 > (numerator 1/2) 1

 (realfix x) → t x : t
Coerces x to a real number. If x satisfies (real/rationalp x), then it returns the argument unchanged. Otherwise, returns 0.

Examples:

 > (realfix 2/5) 2/5 > (realfix (complex 3 2)) 0 > (realfix "5") 0

 (realpart x) → t x : (acl2-numberp x)
Returns the real part of a complex number.

Examples:

 > (realpart (complex 3 2)) 3 > (realpart 1/2) 1/2

 (rem i j) → t i : (real/rationalp i) j : (and (real/rationalp j) (not (eql j 0)))
Calculates the remainder of (/ i j) using truncate.

Examples:

 > (rem 4 2) 0 > (rem 8 3) 2

 (rfix x) → t x : t
Coerces x into a rational number. If x is a rational number, then it returns x unchanged. Otherwise, it returns 0.

Examples:

 > (rfix 2/5) 2/5 > (rfix (complex 3 2)) 0 > (rfix "5") 0

 (round i j) → t i : (real/rationalp i) j : (real/rationalp j)
Rounds (/ i j) to the nearest integer. When the quotient is exactly halfway between to integers, it rounds to the even one.

Examples:

 > (round 4 2) 2 > (round 3 2) 2 > (round 5 2) 2 > (round 4 3) 1

 (signum x) → t x : (real/rationalp x)
Returns 0 if x is 0, -1 if it is negative, and 1 if it is positive.

Examples:

 > (signum 5) 1 > (signum 0) 0 > (signum -5) -1

 (truncate i j) → t i : (real/rationalp i) j : (and (real/rationalp j) (not (eql j 0)))
Computes (/ i j) and rounds down to the nearest integer.

Examples:

 > (truncate 5 2) 2 > (truncate 4 2) 2 > (truncate 19 10) 1 > (truncate 1 10) 0

 (unary-- x) → t x : (acl2-numberp x)
Computes the negative of the input.

Examples:

 > (unary-- 5) -5 > (unary-- -5) 5 > (unary-- (complex 1 -2)) -1+2i

 (unary-/ x) → t x : (and (acl2-numberp x) (not (eql x 0)))
Computes the reciprocal of the input.

Examples:

 > (unary-/ 5) 1/5 > (unary-/ 1/5) 5 > (unary-/ (complex 1 2)) 1/5-2/5i