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-*
| (+ num ...) |
Adds the given numbers together, taking any number of arguments. This is a macro that expands into calls of the function binary-+.
| (- num num) |
Subtracts the given numbers. If only one argument is given, returns the negation of the input.
| (/ num num) |
Divides the first number by the second. If only one argument is given, returns the reciprocal of the input.
| (1+ num) |
Adds 1 to the given number.
Example: | ||
|
| (1- num) |
Subtracts 1 from the given number.
Example: | ||
|
| (binary-* x y) → t |
| x : (acl2-numberp x) |
| y : (acl2-numberp y) |
Takes exactly two numbers and multiplies them together.
Example: | ||
|
| (binary-+ x y) → t |
| x : (acl2-numberp x) |
| y : (acl2-numberp y) |
Takes exactly two numbers and adds them together.
Example: | ||
|
| (/= x y) → t |
| x : (acl2-numberp x) |
| y : (acl2-numberp y) |
Determines if x is less than y.
Determines if x is less than or equal to y.
| (= 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.
Determines if x is greater than y.
Determines if x is greater than or equal to y.
| (acl2-numberp x) |
Returns true if and only if x is a rational or complex rational number.
Examples: | ||||||
|
Determines if z is a complex number consisting of rational parts.
Examples: | ||||||||
|
| (complex/complex-rationalp z) → t |
| z : t |
For most cases, this is simply a macro abbreviating complex-rationalp.
Examples: | ||||||||
|
This is a test for the base case (zero) of recursion on the natural numbers.
Examples: | ||||||||
|
| (minusp x) → t |
| x : (real/rationalp x) |
Determines whether x is a negative number.
Determines if x is a natural number.
Determines if x is odd.
| (plusp x) → t |
| x : (real/rationalp x) |
Determines if x is positive.
Determines if x is a positive integer.
| (rationalp x) |
Determines if x is a rational number.
Examples: | ||||||||
|
| (real/rationalp x) |
In most cases, this is just a macro abbreviating rationalp.
Examples: | ||||
|
| (abs x) → t |
| x : (real/rationalp x) |
Computes the absolute value of x.
| (ceiling i j) → t |
| i : (real/rationalp i) |
| j : (and (real/rationalp j) (not (eql j 0))) |
Creates a complex number with real part n and imaginary part i.
| (conjugate x) → t |
| x : (acl2-numberp x) |
Computes the complex conjugate of x (the result of negating its imaginary part).
| (denominator x) → t |
| x : (rationalp x) |
Returns the divisor of a rational number in lowest terms.
Examples: | ||||||
|
Determines if x is even.
| (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: | ||||||||
|
Raises i to the jth power.
Coerces x to a number. If x is a number, (fix x) returns the argument unchanged. Otherwise, it returns 0.
| (floor i j) → t |
| i : (real/rationalp i) |
| j : (and (real/rationalp j) (not (eql j 0))) |
Coerces x to an integer. If x is an integer, (ifix x) returns the argument unchanged. Otherwise, it returns 0.
| (imagpart i) → t |
| i : (acl2-numberp i) |
Returns the imaginary part of a complex number.
| (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 =.
| (integer-length x) → t |
| x : (integerp x) |
Returns the number of bits in the two’s complement binary representation of x.
Examples: | ||||
|
| (integerp x) |
Determines whether x is an integer.
| (max i j) → t |
| i : (real/rationalp i) |
| j : (real/rationalp j) |
Returns the greater of the two given numbers.
| (min i j) → t |
| i : (real/rationalp i) |
| j : (real/rationalp j) |
Returns the lesser of the two given numbers.
| (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.
Coerces x to a natural number. If x is a natural number, (nfix x) returns the argument unchanged. Otherwise, it returns 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: | ||||
|
Returns the dividend of a rational number in lowest terms.
Coerces x to a real number. If x satisfies (real/rationalp x), then it returns the argument unchanged. Otherwise, returns 0.
| (realpart x) → t |
| x : (acl2-numberp x) |
Returns the real part of a complex number.
| (rem i j) → t |
| i : (real/rationalp i) |
| j : (and (real/rationalp j) (not (eql j 0))) |
Coerces x into a rational number. If x is a rational number, then it returns x unchanged. Otherwise, it returns 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.
| (signum x) → t |
| x : (real/rationalp x) |
Returns 0 if x is 0, -1 if it is negative, and 1 if it is positive.
| (truncate i j) → t |
| i : (real/rationalp i) |
| j : (and (real/rationalp j) (not (eql j 0))) |
| (unary-- x) → t |
| x : (acl2-numberp x) |
Computes the negative of the input.
Computes the reciprocal of the input.