On this page:
*
+
-
/
1+
1-
binary-*
binary-+
/ =
<
<=
=
>
>=
acl2-numberp
complex-rationalp
complex/ complex-rationalp
zp
minusp
natp
oddp
plusp
posp
rationalp
real/ rationalp
abs
ceiling
complex
conjugate
denominator
evenp
explode-nonnegative-integer
expt
fix
floor
ifix
imagpart
int=
integer-length
integerp
max
min
mod
nfix
nonnegative-integer-quotient
numerator
realfix
realpart
rem
rfix
round
signum
truncate
unary--
unary-/
1.4.5 Rational 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

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")

'()

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.

(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")

'()

Determines if x is a rational number.

Examples:

> (rationalp 2/5)

't

> (rationalp 2)

't

> (rationalp (complex 1 2))

'()

> (rationalp "number")

'()

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

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.

(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