FMT1

:(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.