		Search-engine friendly clone of the ACL2 documentation.

Omaps

Values

Oset of the values of an omap.

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

Definitions and Theorems

Function: values

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

Theorem: setp-of-values

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

Theorem: values-when-empty

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