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