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)
        ((equal y 'list)
         (if (stringp x)
             (coerce x 'list)
         (coerce (make-character-list x) 'string))))

Guard for (coerce x y):

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

Also see distributed 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).