		Search-engine friendly clone of the ACL2 documentation.

Make-character-list

coerce to a list of characters

Non-characters in the given list are coerced to the character with code 0.

Function: make-character-list

(defun make-character-list (x)
  (declare (xargs :guard t))
  (cond ((atom x) nil)
        ((characterp (car x))
         (cons (car x)
               (make-character-list (cdr x))))
        (t (cons *null-char*
                 (make-character-list (cdr x))))))

Subtopics

Std/strings/make-character-list: Lemmas about make-character-list in the std/strings library.
Character-list-fix: Inline fixing function for character lists.