		Search-engine friendly clone of the ACL2 documentation.

Omaps

From-alist

Build an omap from an alist.

Signature
(from-alist alist) → map
Arguments: alist — Guard (alistp alist).
Returns: map — Type (mapp map).

If there are duplicate keys in the alist, the leftmost one, with the corresponding value, will be in the resulting omap. This is consistent with the shadowing of alists.

Definitions and Theorems

Function: from-alist

(defun from-alist (alist)
  (declare (xargs :guard (alistp alist)))
  (let ((__function__ 'from-alist))
    (declare (ignorable __function__))
    (cond ((endp alist) nil)
          (t (update (caar alist)
                     (cdar alist)
                     (from-alist (cdr alist)))))))

Theorem: mapp-of-from-alist

(defthm mapp-of-from-alist
  (b* ((map (from-alist alist)))
    (mapp map))
  :rule-classes :rewrite)