		Search-engine friendly clone of the ACL2 documentation.

Built-in-theorems

Built-in-theorems-about-booleans

Built-in-theorems about booleans.

Theorem: booleanp-compound-recognizer

(defthm booleanp-compound-recognizer
        (equal (booleanp x)
               (or (equal x t) (equal x nil)))
        :rule-classes :compound-recognizer)

Theorem: boolean-listp-cons

(defthm boolean-listp-cons
        (equal (boolean-listp (cons x y))
               (and (booleanp x) (boolean-listp y))))

Theorem: boolean-listp-forward

(defthm boolean-listp-forward
        (implies (boolean-listp (cons a lst))
                 (and (booleanp a) (boolean-listp lst)))
        :rule-classes :forward-chaining)

Theorem: boolean-listp-forward-to-symbol-listp

(defthm boolean-listp-forward-to-symbol-listp
        (implies (boolean-listp x)
                 (symbol-listp x))
        :rule-classes :forward-chaining)