(vl-printable-p x) recognizes strings, character lists, numbers, and ordinary characters.
(vl-printable-p x) → *
We use this function as the guard for functions such as vl-print, vl-println, etc. We do not allow
(defun vl-printable-p (x) (declare (xargs :guard t)) (let ((__function__ 'vl-printable-p)) (declare (ignorable __function__)) (or (stringp x) (character-listp x) (acl2-numberp x) (characterp x))))
(defthm vl-printable-p-when-stringp (implies (stringp x) (vl-printable-p x)))
(defthm vl-printable-p-when-character-listp (implies (character-listp x) (vl-printable-p x)))
(defthm vl-printable-p-when-acl2-numberp (implies (acl2-numberp x) (vl-printable-p x)))
(defthm vl-printable-p-when-characterp (implies (characterp x) (vl-printable-p x)))