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)))))))Declarations in ACL2 may occur only where
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
(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.