		Search-engine friendly clone of the ACL2 documentation.

Library-extensions

Omap-theorems

Some theorems about omaps.

Definitions and Theorems

Theorem: lookup-of-update

(defthm omap::lookup-of-update
  (equal (omap::lookup key (omap::update key1 val map))
         (if (equal key key1)
             val
           (omap::lookup key map))))

Theorem: emptyp-of-keys-to-emptyp

(defthm omap::emptyp-of-keys-to-emptyp
  (equal (emptyp (omap::keys map))
         (omap::emptyp map)))