►Dracula:   Reference Manual
►1 ACL2
▼1.4 Functions and Macros
1.4.1 Booleans
1.4.2 Symbols
1.4.3 Strings
1.4.4 Characters
1.4.5 Rational and Complex Arithmetic
1.4.6 Bitwise Operations
1.4.7 Ordinal Arithmetic
1.4.8 Lists
1.4.9 Association Lists
1.4.10 Sets
1.4.11 Trees
1.4.12 Sequences
1.4.13 IO
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-/
    ← prev  up  next → 
1.4.5 Rational and Complex Arithmetic

syntax

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

syntax

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

syntax

(- num num)

Subtracts the given numbers. If only one argument is given, returns the negation of the input.

Examples:

> (- 5)

-5

> (- 5 3)

2

syntax

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

syntax

(1+ num)

Adds 1 to the given number.

Example:

> (1+ 1)

2

syntax

(1- num)

Subtracts 1 from the given number.

Example:

> (1- 1)

0

procedure

(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

procedure

(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

procedure

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

procedure

(< x y) → t

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

Examples:

> (< 1 2)

't

> (< 2 1)

'()

> (< 2 2)

'()

procedure

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

procedure

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

procedure

(> x y) → t

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

Examples:

> (> 1 2)

'()

> (> 2 1)

't

> (> 2 2)

'()

procedure

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

syntax

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

'()

syntax

(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

procedure

(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

procedure

(zp v) → t

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

Examples:

> :eval

:eval: undefined;

 cannot reference undefined identifier

> the-evaluator

the-evaluator: undefined;

 cannot reference undefined identifier

> (zp 0)

zp: undefined;

 cannot reference undefined identifier

> (zp 1)

zp: undefined;

 cannot reference undefined identifier

procedure

(minusp x) → t

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

Examples:

> (minusp 1)

'()

> (minusp -1)

't

procedure

(natp x) → t

  x : t
Determines if x is a natural number.

Examples:

> (natp 1)

't

> (natp 0)

't

> (natp -1)

'()

procedure

(oddp x) → t

  x : (integerp x)
Determines if x is odd.

Examples:

> (oddp 3)

't

> (oddp 2)

'()

procedure

(plusp x) → t

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

Examples:

> (plusp 1)

't

> (plusp -1)

'()

> (plusp 1/2)

't

procedure

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

'()

syntax

(rationalp x)

Determines if x is a rational number.

Examples:

> (rationalp 2/5)

't

> (rationalp 2)

't

> (rationalp (complex 1 2))

'()

> (rationalp "number")

'()

syntax

(real/rationalp x)

In most cases, this is just a macro abbreviating rationalp.

Examples:

> (real/rationalp 2/5)

't

> (real/rationalp "number")

'()

procedure

(abs x) → t

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

Examples:

> (abs 1)

1

> (abs -1)

1

procedure

(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

procedure

(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

procedure

(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

procedure

(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

procedure

(evenp x) → t

  x : (integerp x)
Determines if x is even.

Examples:

> (evenp 1)

'()

> (evenp 2)

't

procedure

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

procedure

(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

procedure

(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

procedure

(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

procedure

(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

procedure

(imagpart i) → t

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

Examples:

> (imagpart (complex 3 2))

2

> (imagpart 5)

0

syntax

(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

procedure

(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

syntax

(integerp x)

Determines whether x is an integer.

Examples:

> (integerp 12)

't

> (integerp '12)

't

> (integerp nil)

'()

procedure

(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

procedure

(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

procedure

(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

procedure

(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

procedure

(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

procedure

(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

procedure

(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

procedure

(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

procedure

(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

procedure

(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

procedure

(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

procedure

(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

procedure

(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

procedure

(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

procedure

(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

    ← prev  up  next →