Major Section: PROGRAMMING
Examples: The symbol INTEGER in (declare (type INTEGER i j k)) is a type-spec. Other type-specs supported by ACL2 include RATIONAL, COMPLEX, (INTEGER 0 127), (RATIONAL 1 *), CHARACTER, and ATOM.
The type-specs and their meanings (when applied to the variable
(declare (type type-spec x)) are given below.
type-spec meaning ATOM (ATOM X) BIT (OR (EQUAL X 1) (EQUAL X 0)) CHARACTER (CHARACTERP X) COMPLEX, (AND (COMPLEX-RATIONALP X) (COMPLEX RATIONAL) (RATIONALP (REALPART X)) (RATIONALP (IMAGPART X))) (COMPLEX type) (AND (COMPLEX-RATIONALP X) (p (REALPART X)) (p (IMAGPART X))) where (p x) is the meaning for type-spec type CONS (CONSP X) INTEGER (INTEGERP X) (INTEGER i j) (AND (INTEGERP X) ; See notes below (<= i X) (<= X j)) (MEMBER x1 ... xn) (MEMBER X '(x1 ... xn)) (MOD i) same as (INTEGER 0 i-1) NIL NIL NULL (EQ X NIL) RATIO (AND (RATIONALP X) (NOT (INTEGERP X))) RATIONAL (RATIONALP X) (RATIONAL i j) (AND (RATIONALP X) ; See notes below (<= i X) (<= X j)) REAL (RATIONALP X) ; (REALP X) in ACL2(r) (REAL i j) (AND (RATIONALP X) ; See notes below (<= i X) (<= X j)) (SATISFIES pred) (pred X) SIGNED-BYTE (INTEGERP X) (SIGNED-BYTE i) same as (INTEGER -2**i-1 (2**i-1)-1) STANDARD-CHAR (STANDARD-CHARP X) STRING (STRINGP X) (STRING max) (AND (STRINGP X) (EQUAL (LENGTH X) max)) SYMBOL (SYMBOLP X) T T UNSIGNED-BYTE same as (INTEGER 0 *) (UNSIGNED-BYTE i) same as (INTEGER 0 (2**i)-1)Notes:
(integer i j) means
(AND (INTEGERP X) (<= i X) (<= X j)).But if
iis the symbol
*, the first inequality is omitted. If
jis the symbol
*, the second inequality is omitted. If instead of being an integer, the second element of the type specification is a list containing an integer,
(i), then the first inequality is made strict. An analogous remark holds for the
REALtype specifiers are similarly generalized.