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

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

Theorem: in-values-when-assoc

(defthm in-values-when-assoc
  (implies (equal (assoc a m) (cons a b))
           (set::in b (values m))))

Theorem: values-of-update-when-not-assoc

(defthm values-of-update-when-not-assoc
  (implies (not (consp (assoc key map)))
           (equal (values (update key val map))
                  (insert val (values map)))))

Theorem: values-of-mfix-map

(defthm values-of-mfix-map
  (equal (values (mfix map))
         (values map)))

Theorem: values-mequiv-congruence-on-map

(defthm values-mequiv-congruence-on-map
  (implies (mequiv map map-equiv)
           (equal (values map) (values map-equiv)))
  :rule-classes :congruence)