BINARY-APPEND

concatenate two lists 
Major Section:  ACL2-BUILT-INS

This binary function implements append, which is a macro in ACL2. See append

The guard for binary-append requires the first argument to be a true-listp.

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