		Search-engine friendly clone of the ACL2 documentation.

Soft-implementation-core

Fun-subst-term/terms

Apply function substitutions to terms.

See the discussion in fun-subst-function.

Function: fun-subst-term

(defun fun-subst-term (fsbs term wrld)
 (declare (xargs :guard (and (fun-substp fsbs)
                             (pseudo-termp term)
                             (plist-worldp wrld))))
 (let ((__function__ 'fun-subst-term))
  (declare (ignorable __function__))
  (if (or (variablep term) (quotep term))
      term
    (let*
       ((fn (fn-symb term))
        (new-fn (if (symbolp fn)
                    (fun-subst-function fsbs fn wrld)
                  (make-lambda (lambda-formals fn)
                               (fun-subst-term fsbs (lambda-body fn)
                                               wrld))))
        (new-args (fun-subst-terms fsbs (fargs term)
                                   wrld)))
      (cons new-fn new-args)))))

Function: fun-subst-terms

(defun fun-subst-terms (fsbs terms wrld)
  (declare (xargs :guard (and (fun-substp fsbs)
                              (pseudo-term-listp terms)
                              (plist-worldp wrld))))
  (let ((__function__ 'fun-subst-terms))
    (declare (ignorable __function__))
    (if (endp terms)
        nil
      (cons (fun-subst-term fsbs (car terms) wrld)
            (fun-subst-terms fsbs (cdr terms)
                             wrld)))))

Definitions and Theorems

Function: fun-subst-term

(defun fun-subst-term (fsbs term wrld)
 (declare (xargs :guard (and (fun-substp fsbs)
                             (pseudo-termp term)
                             (plist-worldp wrld))))
 (let ((__function__ 'fun-subst-term))
  (declare (ignorable __function__))
  (if (or (variablep term) (quotep term))
      term
    (let*
       ((fn (fn-symb term))
        (new-fn (if (symbolp fn)
                    (fun-subst-function fsbs fn wrld)
                  (make-lambda (lambda-formals fn)
                               (fun-subst-term fsbs (lambda-body fn)
                                               wrld))))
        (new-args (fun-subst-terms fsbs (fargs term)
                                   wrld)))
      (cons new-fn new-args)))))

Function: fun-subst-terms

(defun fun-subst-terms (fsbs terms wrld)
  (declare (xargs :guard (and (fun-substp fsbs)
                              (pseudo-term-listp terms)
                              (plist-worldp wrld))))
  (let ((__function__ 'fun-subst-terms))
    (declare (ignorable __function__))
    (if (endp terms)
        nil
      (cons (fun-subst-term fsbs (car terms) wrld)
            (fun-subst-terms fsbs (cdr terms)
                             wrld)))))

Subtopics

Fun-subst-term
Fun-subst-terms