		Search-engine friendly clone of the ACL2 documentation.

Doublets-to-alist

Turn a true list of doublets (i.e. lists of length 2) into the corresponding alist.

This is the inverse of alist-to-doublets.

Definitions and Theorems

Function: doublets-to-alist

(defun doublets-to-alist (doublets)
  (declare (xargs :guard (doublet-listp doublets)))
  (if (endp doublets)
      nil
    (cons (cons (car (first doublets))
                (cadr (first doublets)))
          (doublets-to-alist (rest doublets)))))

Theorem: doublets-to-alist-of-alist-to-doublets

(defthm doublets-to-alist-of-alist-to-doublets
  (implies (alistp x)
           (equal (doublets-to-alist (alist-to-doublets x))
                  x)))

Theorem: alist-to-doublets-of-doublets-to-alist

(defthm alist-to-doublets-of-doublets-to-alist
  (implies (doublet-listp x)
           (equal (alist-to-doublets (doublets-to-alist x))
                  x)))