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)))))))



Some Related Topics



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.  Xargs declarations are only allowed at the top level of
  definitions (defun and defmacro, as shown below).

  (optimize ...) -- for example, (optimize (safety 3)).  This is allowed
  only at the top level of defun forms.  See any Common Lisp
  documentation for more information.
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)
  (FLET ((name args 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.