Apply$-guard
The guard on apply$
The guard on (apply$ fn lst) is (apply$-guard fn lst) which
is extraordinarily weak.
Function: apply$-guard
(defun apply$-guard (fn args)
(declare (xargs :guard t))
(if (atom fn)
(true-listp args)
(apply$-lambda-guard fn args)))
where
Function: apply$-lambda-guard
(defun apply$-lambda-guard (fn args)
(declare (xargs :guard t))
(and (consp fn)
(consp (cdr fn))
(true-listp args)
(equal (len (cadr fn)) (length args))))
This guard is just strong enough to allow the definitions of the functions
in the apply$ clique to be guard verified. It does not guarantee that
fn is tame or well-formed or that args satisfy the guard of
fn. The last condition is in fact impossible to state given the untyped
nature of ACL2. Thus, (apply$ fn args) has to check tameness,
well-formedness, guard verified, and that fn's guard is satisfied by
args when the apply$ is executed in the evaluation theory.
The issue of guards and guard verification of definitions involving
apply$ is further discussed in apply$ and in verify-guards.
