		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))