		Search-engine friendly clone of the ACL2 documentation.

Std/basic

Good-valuep

Check if a value is ``good''.

Signature
(good-valuep x) → yes/no
Returns: yes/no — Type (booleanp 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.

Definitions and Theorems

Function: good-valuep

(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))))))

Theorem: booleanp-of-good-valuep

(defthm booleanp-of-good-valuep
  (b* ((yes/no (good-valuep x)))
    (booleanp yes/no))
  :rule-classes :rewrite)