		Search-engine friendly clone of the ACL2 documentation.

Std/system/term-transformations

Fsublis-fn-simple

Variant of sublis-fn-simple that performs no simplification.

Signature
(fsublis-fn-simple alist term) → new-term
Arguments: alist — Guard (symbol-symbol-alistp alist).; term — Guard (pseudo-termp term).
Returns: new-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: fsublis-fn-simple

(defun fsublis-fn-simple (alist term)
  (declare (xargs :guard (and (symbol-symbol-alistp alist)
                              (pseudo-termp term))))
  (let ((__function__ 'fsublis-fn-simple))
    (declare (ignorable __function__))
    (mv-let (vars result)
            (fsublis-fn-rec alist term nil t)
      (assert$ (null vars) result))))