		Search-engine friendly clone of the ACL2 documentation.

Svex-focused-equivalence-checking

My-replace-assoc

Signature
(my-replace-assoc key val alist) → *
Arguments: key — Guard (symbolp key).

Definitions and Theorems

Function: my-replace-assoc

(defun my-replace-assoc (key val alist)
  (declare (xargs :guard (symbolp key)))
  (let ((__function__ 'my-replace-assoc))
    (declare (ignorable __function__))
    (if (atom alist)
        alist
      (if (and (consp (car alist))
               (eq key (caar alist)))
          (cons (cons key val) (cdr alist))
        (cons (car alist)
              (my-replace-assoc key val (cdr alist)))))))