		Search-engine friendly clone of the ACL2 documentation.

Omaps

Keys

Oset of the keys of an omap.

Signature
(keys map) → keys
Arguments: map — Guard (mapp map).
Returns: keys — Type (setp keys).

Definitions and Theorems

Function: keys

(defun keys (map)
       (declare (xargs :guard (mapp map)))
       (let ((__function__ 'keys))
            (declare (ignorable __function__))
            (cond ((empty map) nil)
                  (t (mv-let (key val)
                             (head map)
                             (declare (ignore val))
                             (insert key (keys (tail map))))))))

Theorem: setp-of-keys

(defthm setp-of-keys
        (b* ((keys (keys map))) (setp keys))
        :rule-classes :rewrite)

Theorem: keys-when-empty

(defthm keys-when-empty
        (implies (empty map)
                 (equal (keys map) nil))
        :rule-classes (:rewrite :type-prescription))