COERCE

coerce a character list to a string and a string to a list 
Major Section:  ACL2-BUILT-INS

Completion Axiom (completion-of-coerce): 

(equal (coerce x y)
       (cond
        ((equal y 'list)
         (if (stringp x)
             (coerce x 'list)
           nil))
        (t
         (coerce (make-character-list x) 'string))))

Guard for (coerce x y): 

(if (equal y 'list)
    (stringp x)
  (if (equal y 'string)
      (character-listp x)
    nil))

Also see community book books/misc/fast-coerce.lisp, contributed by Jared Davis, for a version of coerce that may be faster for Common Lisp implementations other than CCL 1.3 or later, if the second argument is 'list (for coercing a string to a list).