On this page:
*
+
-
/
1+
1-
binary-*
binary-+
/ =
<
<=
=
>
>=
acl2-numberp
complex-rationalp
complex/ complex-rationalp
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-/
Version: 4.1
2.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. Takes one or more arguments.

Examples:

  > (- 5)

  -5

  > (- 5 3)

  2

  > (- 10 5 3 1)

  eval:1234:0: -: Expects only one or two arguments, but

  given 4 in: (- 10 5 3 1)

  > (-)

  eval:1237:0: -: Expects only one or two arguments, but

  given 0 in: (-)

(/ 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

  > (/)

  eval:1246:0: /: Expected one or two arguments, but got 0

  in: (/)

  > (/ 100 5 2)

  eval:1249:0: /: Expected one or two arguments, but got 3

  in: (/ 100 5 2)

(1+ num)

Adds 1 to the given number.

Examples:

  > (1+ 1)

  2

  > (1+)

  eval:1255:0: 1+: Expected 1 arguments, but got 0 in: (1+)

  > (1+ 1 2)

  eval:1258:0: 1+: Expected 1 arguments, but got 2 in: (1+ 1

  2)

(1- num)

Subtracts 1 from the given number.

Examples:

  > (1- 1)

  0

  > (1-)

  eval:1264:0: 1-: Expected 1 arguments, but got 0 in: (1-)

  > (1- 1 2)

  eval:1267:0: 1-: Expected 1 arguments, but got 2 in: (1- 1

  2)

(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-* 1)

  eval:1273:0: binary-*: Expected 2 arguments, but got 1 in:

  (binary-* 1)

  > (binary-* "5" 10)

  *: expects type <number> as 1st argument, given: "5"; other

  arguments were: 10

(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

  > (binary-+ 1)

  eval:1282:0: binary-+: Expected 2 arguments, but got 1 in:

  (binary-+ 1)

  > (binary-+ "5" 10)

  +: expects type <number> as 1st argument, given: "5"; other

  arguments were: 10

(/= 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

  > (/= "3" 2)

  Dracula program broke the contract (-> acl2-number?

  acl2-number? any) on here; expected <acl2-number?>, given:

  "3"

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

(minusp x)  t

  x : (real/rationalp x)

Determines whether x is a negative number.

Examples:

  > (minusp 1)

  ()

  > (minusp -1)

  t

  > (minusp (complex 1 2))

  Dracula program broke the contract (-> rational? any) on

  here; expected <rational?>, given: 1+2i

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

  ()

  > (oddp 1/2)

  Dracula program broke the contract (-> integer? any) on

  here; expected <integer?>, given: 1/2

(plusp x)  t

  x : (real/rationalp x)

Determines if x is positive.

Examples:

  > (plusp 1)

  t

  > (plusp -1)

  ()

  > (plusp 1/2)

  t

  > (plusp (complex 1 2))

  Dracula program broke the contract (-> rational? any) on

  here; expected <rational?>, given: 1+2i

(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

  > (abs (complex 1 1))

  Dracula program broke the contract (-> rational? any) on

  here; expected <rational?>, given: 1+1i

(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

  > (ceiling "5" 3)

  /: expects type <number> as 1st argument, given: "5"; other

  arguments were: 3

(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

  > (complex (complex 2 3) 5)

  2+8i

(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

  > (denominator (complex 1 2))

  denominator: expects argument of type <rational number>;

  given 1+2i

(evenp x)  t

  x : (integerp x)

Determines if x is even.

Examples:

  > (evenp 1)

  ()

  > (evenp 2)

  t

  > (evenp 1/2)

  Dracula program broke the contract (-> integer? any) on

  here; expected <integer?>, given: 1/2

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

  > (explode-nonnegative-integer -100 16 nil)

  Dracula program broke the contract (->

  natural-number/c (or/c (=/c 2) (=/c 8) (=/c 10) (=/c

  16)) any/c any) on here; expected <natural-number/c>,

  given: -100

(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

  > (expt 10 1/2)

  Dracula program broke the contract (-> acl2-number?

  integer? any) on here; expected <integer?>, given: 1/2

  > (expt 0 -2)

  expt: undefined for 0 and -2

(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

  > (floor "5" 3)

  Dracula program broke the contract (-> rational?

  non-zero-real/rational? any) on here; expected <rational?>,

  given: "5"

(ifix [x t])

#<procedure: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

  > (imagpart "5")

  imag-part: expects argument of type <number>; given "5"

(int= i j)

Checks to see if the two integers i and j are equal. This is like equal and =, but with the 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

  > (int= 1/2 1/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

  > (integer-length 1/2)

  0

(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

  > (max 4)

  eval:1606:0: max: Expected 2 arguments, but got 1 in: (max

  4)

  > (max (complex 1 2) 2)

  Dracula program broke the contract (-> rational? rational?

  any) on here; expected <rational?>, given: 1+2i

(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

  > (min 4)

  eval:1618:0: min: Expected 2 arguments, but got 1 in: (min

  4)

  > (min (complex 1 2))

  eval:1621:0: min: Expected 2 arguments, but got 1 in: (min

  (complex 1 2))

(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

  > (mod 8 0)

  Dracula program broke the contract (-> rational?

  non-zero-real/rational? any) on here; expected

  <non-zero-real/rational?>, given: 0

(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

  > (numerator (complex 1 2))

  numerator: expects argument of type <rational number>;

  given 1+2i

(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

  > (rem (complex 1 2) 3)

  numerator: expects argument of type <rational number>;

  given 1/3+2/3i

(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

  > (round (complex 1 2) 3)

  Dracula program broke the contract (-> rational? rational?

  any) on here; expected <rational?>, given: 1/3+2/3i

(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

  > (truncate (complex 1 2) 3)

  numerator: expects argument of type <rational number>;

  given 1/3+2/3i

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

  -: expects argument of type <number>; given "5"

(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

  > (unary-/ 0)

  Dracula program broke the contract (->

  non-zero-acl2-number? any) on here; expected

  <non-zero-acl2-number?>, given: 0

  > (unary-/ "5")

  Dracula program broke the contract (->

  non-zero-acl2-number? any) on here; expected

  <non-zero-acl2-number?>, given: "5"