		Search-engine friendly clone of the ACL2 documentation.

Omaps

Update*

Update a map with another map.

Signature
(update* new old) → map
Arguments: new — Guard (mapp new).; old — Guard (mapp old).
Returns: map — Type (mapp map).

This lifts update from a single key and value to a set of key-value pairs, passed as the first argument map. If a key is in the second but not in the first map, the key is present in the result, with the same value as in the second map. If a key is in the first but not in the second map, the key is present in the result, with the same value as in the first map. If a key is present in both maps, it is present in the result, with the same value as in the first map; i.e. the first map ``wins''. There are no other keys in the result.

Definitions and Theorems

Function: update*

(defun update* (new old)
  (declare (xargs :guard (and (mapp new) (mapp old))))
  (let ((__function__ 'update*))
    (declare (ignorable __function__))
    (cond ((emptyp new) (mfix old))
          (t (mv-let (new-key new-val)
                     (head new)
               (update new-key
                       new-val (update* (tail new) old)))))))

Theorem: mapp-of-update*

(defthm mapp-of-update*
  (b* ((map (update* new old)))
    (mapp map))
  :rule-classes :rewrite)

Theorem: update*-when-left-emptyp

(defthm update*-when-left-emptyp
  (implies (emptyp new)
           (equal (update* new old) (mfix old))))

Theorem: update*-when-right-emptyp

(defthm update*-when-right-emptyp
  (implies (emptyp old)
           (equal (update* new old) (mfix new))))