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 let s and our er-let* expands into nested
mv-let s) then declarations are permitted as handled by the macros
involved.
Declare is defined in Common Lisp. See any Common Lisp
documentation for more information.