		Search-engine friendly clone of the ACL2 documentation.

Omaps

From-lists

Build an omap from a list of keys and a list of corresponding values.

Signature
(from-lists keys vals) → map
Arguments: keys — Guard (true-listp keys).; vals — Guard (true-listp vals).
Returns: map — Type (mapp map).

If there are duplicate keys in the first list, the leftmost key, and the corresponding value, will be in the resulting omap.

Definitions and Theorems

Function: from-lists

(defun from-lists (keys vals)
       (declare (xargs :guard (and (true-listp keys)
                                   (true-listp vals))))
       (declare (xargs :guard (= (len keys) (len vals))))
       (let ((__function__ 'from-lists))
            (declare (ignorable __function__))
            (cond ((endp keys) nil)
                  (t (update (car keys)
                             (car vals)
                             (from-lists (cdr keys) (cdr vals)))))))

Theorem: mapp-of-from-lists

(defthm mapp-of-from-lists
        (b* ((map (from-lists keys vals)))
            (mapp map))
        :rule-classes :rewrite)

Theorem: from-lists-of-list-fix-keys

(defthm from-lists-of-list-fix-keys
        (equal (from-lists (list-fix keys) vals)
               (from-lists keys vals)))

Theorem: from-lists-list-equiv-congruence-on-keys

(defthm from-lists-list-equiv-congruence-on-keys
        (implies (list-equiv keys keys-equiv)
                 (equal (from-lists keys vals)
                        (from-lists keys-equiv vals)))
        :rule-classes :congruence)

Theorem: from-lists-of-list-fix-vals

(defthm from-lists-of-list-fix-vals
        (equal (from-lists keys (list-fix vals))
               (from-lists keys vals)))

Theorem: from-lists-list-equiv-congruence-on-vals

(defthm from-lists-list-equiv-congruence-on-vals
        (implies (list-equiv vals vals-equiv)
                 (equal (from-lists keys vals)
                        (from-lists keys vals-equiv)))
        :rule-classes :congruence)