TYPE-SPEC

Major Section:  DECLARE

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
(AND type1 ... typek)  (AND (p1 X) ... (pk X))
                       where (pj x) is the meaning for type-spec typej
ATOM                   (ATOM X)
BIT                    (OR (EQUAL X 1) (EQUAL X 0))
CHARACTER              (CHARACTERP X)
COMPLEX                (AND (COMPLEX-RATIONALP X)
                            (RATIONALP (REALPART X))
                            (RATIONALP (IMAGPART X)))
(COMPLEX RATIONAL)     same as COMPLEX, above
(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
(NOT type)             (NOT (p X))
                       where (p x) is the meaning for type-spec type
NULL                   (EQ X NIL)
(OR type1 ... typek)   (OR (p1 X) ... (pk X))
                       where (pj x) is the meaning for type-spec typej
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) ; Lisp requires a unary function, not a macro
SIGNED-BYTE            (INTEGERP X)
(SIGNED-BYTE i)        same as (INTEGER k m) where k=-2^(i-1), m=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)

In general, (integer i j) means

     (AND (INTEGERP X)
          (<= i X)
          (<= X j)).