		Search-engine friendly clone of the ACL2 documentation.

Apply-term*

Apply a function symbol or a lambda expression to zero or more terms, obtaining a term.

This utility is similar to cons-term*, but it performs a beta reduction when fn is a lambda expressions. It is a macro version of apply-term.

Macro: apply-term*

(defmacro apply-term* (fn &rest terms)
  (cons 'apply-term
        (cons fn (cons (cons 'list terms) 'nil))))