Check if a value is ``good''.
(good-valuep x) → yes/no
Check whether a value is either a good atom (i.e. a number, a character, a string, or a symbol) or a cons pair whose car and cdr are recursively good values. That is, check whether a value neiher is a bad atom nor contains (directly or indirectly) bad atoms.
These good values are the only ones that can be constructed in execution. However, in the ACL2 logic, there may be bad atoms, or cons pairs that contain, directly or indirectly, bad atoms.
(defun good-valuep (x) (declare (xargs :guard t)) (let ((__function__ 'good-valuep)) (declare (ignorable __function__)) (or (acl2-numberp x) (characterp x) (stringp x) (symbolp x) (and (consp x) (good-valuep (car x)) (good-valuep (cdr x))))))
(defthm booleanp-of-good-valuep (b* ((yes/no (good-valuep x))) (booleanp yes/no)) :rule-classes :rewrite)