Pairlis$
Zipper together two lists
The Common Lisp language allows its pairlis function to
construct an alist in any order! So we have to define our own version,
pairlis$. It returns the list of pairs obtained by consing
together successive respective members of the given lists until the first list
runs out. (Hence in particular, if the second argument is nil then each
element of the first argument is paired with nil.)
The guard for pairlis$ requires that its arguments are true
lists.
Function: pairlis$
(defun pairlis$ (x y)
(declare (xargs :guard (and (true-listp x) (true-listp y))))
(mbe :logic (cond ((endp x) nil)
(t (cons (cons (car x) (car y))
(pairlis$ (cdr x) (cdr y)))))
:exec (pairlis$-tailrec x y nil)))Subtopics
- Std/alists/pairlis$
- Lemmas about pairlis$ available in the std/alists
library.
