Possibly optimized way to reverse a character list and coerce it to a string.
(rchars-to-string rchars) is logically equal to
(reverse (implode rchars))
We leave it enabled and would not expect to ever reason about it. This operation is useful as the final step in a string-building strategy where characters are accumulated onto a list in reverse order; see for instance revappend-chars.
When you just load books like
But if you are willing to accept a trust tag, then you may optionally load the book:
(include-book "str/fast-cat" :dir :system)
This may improve the performance of
(defun rchars-to-string (rchars) (declare (xargs :guard (character-listp rchars))) (reverse (the string (coerce rchars 'string))))