		Search-engine friendly clone of the ACL2 documentation.

Std/system/term-transformations

Apply-term

Apply a function symbol or a lambda expression to a list of terms, obtaining a term.

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

This utility is similar to cons-term, but it performs a beta reduction when fn is a lambda expression.

Definitions and Theorems

Function: apply-term

(defun apply-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__ 'apply-term))
    (declare (ignorable __function__))
    (cond ((symbolp fn) (cons-term fn terms))
          (t (subcor-var (lambda-formals fn)
                         terms (lambda-body fn))))))