zipper together two lists
Major Section:  ACL2-BUILT-INS

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.

To see the ACL2 definition of this function, see pf.