		Search-engine friendly clone of the ACL2 documentation.

Std/system/term-transformations

Fapply-term

Variant of apply-term that performs no simplification.

Signature
(fapply-term fn terms) → term
Arguments: fn — Guard (pseudo-termfnp fn).; terms — Guard (pseudo-term-listp terms).
Returns: term — A pseudo-termp.

The meaning of the starting f in the name of this utility is analogous to fcons-term compared to cons-term.

Definitions and Theorems

Function: fapply-term

(defun fapply-term (fn terms)
  (declare (xargs :guard (and (pseudo-termfnp fn)
                              (pseudo-term-listp terms))))
  (declare (xargs :guard (or (symbolp fn)
                             (= (len terms)
                                (len (lambda-formals fn))))))
  (let ((__function__ 'fapply-term))
    (declare (ignorable __function__))
    (cond ((symbolp fn) (fcons-term fn terms))
          (t (fsubcor-var (lambda-formals fn)
                          terms (lambda-body fn))))))