		Search-engine friendly clone of the ACL2 documentation.

Std/system/term-transformations

Fsublis-fn

Variant of sublis-fn that performs no simplification.

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

(defun fsublis-fn (alist term bound-vars)
  (declare (xargs :guard (and (symbol-alistp alist)
                              (pseudo-termp term)
                              (symbol-listp bound-vars))))
  (let ((__function__ 'fsublis-fn))
    (declare (ignorable __function__))
    (fsublis-fn-rec alist term bound-vars t)))