Variant of apply-unary-to-terms that performs no simplification.
(fapply-unary-to-terms fn terms) → applied-terms
The meaning of the starting
Function:
(defun fapply-unary-to-terms-aux (fn terms rev-result) (declare (xargs :guard (and (pseudo-termfnp fn) (pseudo-term-listp terms) (pseudo-term-listp rev-result)))) (declare (xargs :guard (or (symbolp fn) (= 1 (len (lambda-formals fn)))))) (let ((__function__ 'fapply-unary-to-terms-aux)) (declare (ignorable __function__)) (cond ((endp terms) (reverse rev-result)) (t (fapply-unary-to-terms-aux fn (cdr terms) (cons (fapply-term* fn (car terms)) rev-result))))))
Function:
(defun fapply-unary-to-terms (fn terms) (declare (xargs :guard (and (pseudo-termfnp fn) (pseudo-term-listp terms)))) (declare (xargs :guard (or (symbolp fn) (= 1 (len (lambda-formals fn)))))) (let ((__function__ 'fapply-unary-to-terms)) (declare (ignorable __function__)) (fapply-unary-to-terms-aux fn terms nil)))