:(str alist col co-channel state evisc) => (mv col state)
Major Section: ACL2-BUILT-INS
See fmt for further explanation, including documentation of the tilde-directives.