DECLARE

declarations
Major Section:  PROGRAMMING

Examples:
(declare (ignore x y z))
(declare (ignore 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.

(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.