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 x
as in (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:
In general, (integer i j) means
(AND (INTEGERP X)
(<= i X)
(<= X j)).
But if i is the symbol *, the first inequality is omitted. If j
is 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 (j) case. The RATIONAL
and REAL type specifiers are similarly generalized.
