Numbers
Numbers in ACL2 and operations on them
See numbers-introduction for introductory background. See arithmetic for libraries of books for arithmetic reasoning.
Subtopics
- Natp
- A recognizer for the natural numbers
- Unsigned-byte-p
- Recognizer for natural numbers that fit in a specified bit width
- Posp
- A recognizer for the positive integers
- +
- Addition macro
- Bitp
- A recognizer for the set of bits, {0,1}
- Zero-test-idioms
- How to test for 0
- Nat-listp
- Recognizer for a true list of natural numbers
- Integerp
- Recognizer for whole numbers
- <
- Less-than
- *
- Multiplication macro
- Zp
- Testing a ``natural'' against 0
- -
- Macro for subtraction and negation
- Signed-byte-p
- Recognizer for signed integers that fit in a specified bit width
- Logbitp
- The ith bit of an integer
- Expt
- Exponential function
- Ash
- Arithmetic shift operation
- Rationalp
- Recognizer for rational numbers (ratios and integers)
- Sharp-f-reader
- Read a rational number in floating-point (scientific notation)
syntax
- Logand
- Bitwise logical `and' of zero or more integers
- =
- Test equality of two numbers
- <=
- Less-than-or-equal test
- Floor
- Division returning an integer by truncating toward negative infinity
- Random$
- Obtain a random value
- Nfix
- Coerce to a natural number
- Truncate
- Division returning an integer by truncating toward 0
- Complex
- Create an ACL2 number
- Numbers-introduction
- Numbers in ACL2
- Code-char
- The character corresponding to a given numeric code
- Integer-length
- Number of bits in two's complement integer representation
- Zip
- Testing an ``integer'' against 0
- Logior
- Bitwise logical inclusive or of zero or more integers
- Sharp-u-reader
- Allow underscore characters in numbers
- Char-code
- The numeric code for a given character
- Unary--
- Arithmetic negation function
- Integer-listp
- Recognizer for a true list of integers
- Boole$
- Perform a bit-wise logical operation on 2 two's complement integers
- /
- Macro for division and reciprocal
- Mod
- Remainder using floor
- Logxor
- Bitwise logical exclusive or of zero or more integers
- Lognot
- Bitwise not of a two's complement number
- Integer-range-p
- Recognizer for integers between two bounds.
- Ifix
- Coerce to an integer
- ACL2-numberp
- Recognizer for numbers
- Ceiling
- Division returning an integer by truncating toward positive infinity
- Mod-expt
- Exponential function
- Round
- Division returning an integer by rounding off
- Logeqv
- Bitwise logical equivalence of zero or more integers
- Explode-nonnegative-integer
- The list of characters in the radix-r form of a number
- Max
- The larger of two numbers
- Evenp
- Test whether an integer is even
- Nonnegative-integer-quotient
- Natural number division function
- Zerop
- Test an acl2-number against 0
- Abs
- The absolute value of a real number
- Fix
- Coerce to a number
- Allocate-fixnum-range
- Set aside fixnums in GCL
- Rem
- Remainder using truncate
- 1+
- Increment by 1
- Pos-listp
- Recognizer for a true list of positive integers
- Signum
- Indicator for positive, negative, or zero
- Real/rationalp
- Recognizer for rational numbers (including real number in ACL2(r))
- Rational-listp
- Recognizer for a true list of rational numbers
- Rfix
- Coerce to a rational number
- >=
- Greater-than-or-equal test
- >
- Greater-than test
- Logcount
- Number of ``on'' bits in a two's complement number
- ACL2-number-listp
- Recognizer for a true list of numbers
- /=
- Test inequality of two numbers
- Unary-/
- Reciprocal function
- Complex/complex-rationalp
- Recognizer for complex numbers
- Logtest
- Test if two integers share a `1' bit
- Logandc1
- Bitwise logical `and' of two ints, complementing the first
- Logorc1
- Bitwise logical inclusive or of two ints, complementing the first
- Logandc2
- Bitwise logical `and' of two ints, complementing the second
- 1-
- Decrement by 1
- Numerator
- Dividend of a ratio in lowest terms
- Logorc2
- Bitwise logical inclusive or of two ints, complementing the second
- Denominator
- Divisor of a ratio in lowest terms
- The-number
- Coerce an expected number to a number
- Realfix
- Coerce to a real number
- Complex-rationalp
- Recognizes complex rational numbers
- Min
- The smaller of two numbers
- Lognor
- Bitwise logical `nor' of two integers
- Zpf
- Testing a nonnegative fixnum against 0
- Oddp
- Test whether an integer is odd
- Minusp
- Test whether a number is negative
- Lognand
- Bitwise logical `nand' of two integers
- Imagpart
- Imaginary part of a complex number
- Conjugate
- Complex number conjugate
- Int=
- Test equality of two integers
- Realpart
- Real part of a complex number
- Plusp
- Test whether a number is positive
