		Search-engine friendly clone of the ACL2 documentation.

Omaps

Delete

Remove a key, and associated value, from an omap.

Signature
(delete key map) → map1
Arguments: map — Guard (mapp map).
Returns: map1 — Type (mapp map1).

This is similar to set::delete for osets.

Definitions and Theorems

Function: delete

(defun delete (key map)
  (declare (xargs :guard (mapp map)))
  (let ((__function__ 'delete))
    (declare (ignorable __function__))
    (cond ((emptyp map) nil)
          (t (mv-let (key0 val0)
                     (head map)
               (cond ((equal key key0) (tail map))
                     (t (update key0
                                val0 (delete key (tail map))))))))))

Theorem: mapp-of-delete

(defthm mapp-of-delete
  (b* ((map1 (delete key map)))
    (mapp map1))
  :rule-classes :rewrite)

Theorem: delete-when-emptyp

(defthm delete-when-emptyp
  (implies (emptyp map)
           (equal (delete key map) nil)))

Theorem: delete-of-mfix-map

(defthm delete-of-mfix-map
  (equal (delete key (mfix map))
         (delete key map)))

Theorem: delete-mequiv-congruence-on-map

(defthm delete-mequiv-congruence-on-map
  (implies (mequiv map map-equiv)
           (equal (delete key map)
                  (delete key map-equiv)))
  :rule-classes :congruence)