		Search-engine friendly clone of the ACL2 documentation.

Def-gl-rule

Find-and-remove-key

Remove keyword key and associated value from list lst

Signature
(find-and-remove-key key lst) → (mv * *)

Definitions and Theorems

Function: find-and-remove-key

(defun find-and-remove-key (key lst)
 (declare (xargs :guard t))
 (let ((__function__ 'find-and-remove-key))
  (declare (ignorable __function__))
  (cond
   ((atom lst) (mv nil lst))
   ((and (equal (car lst) key)
         (atom (cdr lst)))
    (mv
     (er
      hard? __function__
      "Car of lst matches key, when there is no associated value in
                  the lst.  Car is: ~x0.  Lst is: ~x1"
      (car lst)
      lst)
     nil))
   ((equal (car lst) key)
    (mv (cadr lst) (cddr lst)))
   (t (mv-let (val recur-lst)
              (find-and-remove-key key (cdr lst))
        (mv val (cons (car lst) recur-lst)))))))