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.
