		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 ((empty 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-empty

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

Theorem: update*-when-right-empty

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