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.