Variant of sublis-fn-lst-simple that performs no simplification.
(fsublis-fn-lst-simple alist terms) → new-terms
The meaning of the starting
Function:
(defun fsublis-fn-lst-simple (alist terms) (declare (xargs :guard (and (symbol-symbol-alistp alist) (pseudo-term-listp terms)))) (let ((__function__ 'fsublis-fn-lst-simple)) (declare (ignorable __function__)) (mv-let (vars result) (sublis-fn-rec-lst alist terms nil t) (assert$ (null vars) result))))