		Search-engine friendly clone of the ACL2 documentation.

System-level-marking-view-proof-utilities

Replace-element

Signature
(replace-element x y lst) → *

Definitions and Theorems

Function: replace-element

(defun replace-element (x y lst)
  (declare (xargs :guard t))
  (let ((__function__ 'replace-element))
    (declare (ignorable __function__))
    (if (atom lst)
        lst
      (if (equal (car lst) x)
          (cons y (replace-element x y (cdr lst)))
        (cons (car lst)
              (replace-element x y (cdr lst)))))))

Theorem: true-listp-of-replace-element

(defthm true-listp-of-replace-element
  (implies (true-listp lst)
           (true-listp (replace-element x y lst))))