DECLARE

declarations
Major Section:  PROGRAMMING

Examples:
(declare (ignore x y z))
(declare (ignorable x y z)
         (type integer i j k)
         (type (satisfies integerp) m1 m2))
(declare (xargs :guard (and (integerp i)
                            (<= 0 i))
                :guard-hints (("Goal" :use (:instance lemma3
                                              (x (+ i j)))))))

General Form: (declare d1 ... dn) where, in ACL2, each di is of one of the following forms:

(ignore v1 ... vn) -- where each vi is a variable introduced in the immediately superior lexical environment. These variables must not occur free in the scope of the declaration.

(ignorable v1 ... vn) -- where each vi is a variable introduced in the immediately superior lexical environment. These variables need not occur free in the scope of the declaration. This declaration can be useful for inhibiting compiler warnings.

(type type-spec v1 ... vn) -- where each vi is a variable introduced in the immediately superior lexical environment and type-spec is a type specifier (as described in the documentation for type-spec).

(xargs :key1 val1 ... :keyn valn) -- where the legal values of the keyi's and their respective vali's are described in the documentation for xargs.

Declarations in ACL2 may occur only where dcl occurs below:
  (DEFUN name args doc-string dcl ... dcl body)
  (DEFMACRO name args doc-string dcl ... dcl body)
  (LET ((v1 t1) ...) dcl ... dcl body)
  (MV-LET (v1 ...) term dcl ... dcl body)
Of course, if a form macroexpands into one of these (as let* expands into nested lets and our er-let* expands into nested mv-lets) then declarations are permitted as handled by the macros involved.

Declare is defined in Common Lisp. See any Common Lisp documentation for more information.