Version: 4.1.4.3
##### 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.

 Examples: > (1+ 1) 2

 (1- num)

Subtracts 1 from the given number.

 Examples: > (1- 1) 0

 (binary-* x y) → t x : (acl2-numberp x) y : (acl2-numberp y)

Takes exactly two numbers and multiplies them together.

 Examples: > (binary-* 9 8) 72

 (binary-+ x y) → t x : (acl2-numberp x) y : (acl2-numberp y)

Takes exactly two numbers and adds them together.

 Examples: > (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).

 Examples: > (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