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
together successive respective members of the given lists until the
first list runs out. (Hence in particular, if the second argument
nil then each element of the first argument is paired with
The guard for
pairlis$ requires that its arguments are true lists.
To see the ACL2 definition of this function, see pf.