		Search-engine friendly clone of the ACL2 documentation.

Atc-term-recognizers

Atc-boolean-termp

Recognize expression terms returning booleans.

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

We just check whether the term is a call of a boolean-from-<type> function or a call of and or or.

Definitions and Theorems

Function: atc-boolean-termp

(defun atc-boolean-termp (term)
  (declare (xargs :guard (pseudo-termp term)))
  (let ((__function__ 'atc-boolean-termp))
    (declare (ignorable __function__))
    (b* (((mv andp & &) (check-and-call term))
         ((when andp) t)
         ((mv orp & &) (check-or-call term))
         ((when orp) t))
      (case-match term
        ((fn . &)
         (if (member-eq fn *atc-boolean-from-type-fns*)
             t
           nil))
        (& nil)))))

Theorem: booleanp-of-atc-boolean-termp

(defthm booleanp-of-atc-boolean-termp
  (b* ((yes/no (atc-boolean-termp term)))
    (booleanp yes/no))
  :rule-classes :rewrite)