Inline fixing function for character lists.
(character-list-fix x) → *
This is identical to make-character-list except that the
guard requires that
Function:
(defun character-list-fix$inline (x) (declare (xargs :guard (character-listp x))) (let ((acl2::__function__ 'character-list-fix)) (declare (ignorable acl2::__function__)) (mbe :logic (make-character-list x) :exec x)))