		Search-engine friendly clone of the ACL2 documentation.

Deftrans

Take-pairs

Signature
(take-pairs list) → alist
Arguments: list — Guard (true-listp list).
Returns: alist — Type (alistp alist).

Definitions and Theorems

Function: take-pairs

(defun take-pairs (list)
  (declare (xargs :guard (true-listp list)))
  (let ((__function__ 'take-pairs))
    (declare (ignorable __function__))
    (if (endp list)
        nil
      (if (consp (rest list))
          (cons (cons (first list) (second list))
                (take-pairs (rest (rest list))))
        (list (cons (first list) nil))))))

Theorem: alistp-of-take-pairs

(defthm alistp-of-take-pairs
  (b* ((alist (take-pairs list)))
    (alistp alist))
  :rule-classes :rewrite)