		Search-engine friendly clone of the ACL2 documentation.

Good-pseudo-termp

Check if a pseudo-term only contains good values, i.e. no bad atoms.

Signature
(good-pseudo-termp term) → yes/no
Arguments: term — Guard (pseudo-termp term).
Returns: yes/no — Type (booleanp yes/no).

That is, check if every value of every quoted constant in the term satisfies good-valuep.

Theorem: return-type-of-good-pseudo-termp.yes/no

(defthm return-type-of-good-pseudo-termp.yes/no
        (b* ((?yes/no (good-pseudo-termp term)))
            (booleanp yes/no))
        :rule-classes :rewrite)

Theorem: return-type-of-good-pseudo-term-listp.yes/no

(defthm return-type-of-good-pseudo-term-listp.yes/no
        (b* ((?yes/no (good-pseudo-term-listp terms)))
            (booleanp yes/no))
        :rule-classes :rewrite)

Subtopics

Good-pseudo-term-listp