		Search-engine friendly clone of the ACL2 documentation.

Atc-term-recognizers

Atc-stmt-noncval-termp

Recognize statement terms that are not expression terms returning C values.

Signature
(atc-stmt-noncval-termp term wrld) → yes/no
Arguments: term — Guard (pseudo-termp term).; wrld — Guard (plist-worldp wrld).
Returns: yes/no — Type (booleanp yes/no).

We just check if the term is an if, an mv, a let, an mv-let, or a call of a recursive function, which we therefore assume to be a target function.

Definitions and Theorems

Function: atc-stmt-noncval-termp

(defun atc-stmt-noncval-termp (term wrld)
  (declare (xargs :guard (and (pseudo-termp term)
                              (plist-worldp wrld))))
  (let ((__function__ 'atc-stmt-noncval-termp))
    (declare (ignorable __function__))
    (b* (((mv ifp & & &) (check-if-call term))
         ((when ifp) t)
         ((mv mvp &) (check-list-call term))
         ((when mvp) t)
         ((mv mv-letp & & & & & &)
          (check-mv-let-call term))
         ((when mv-letp) t))
      (case-match term
        ((fn . &)
         (or (consp fn)
             (consp (irecursivep+ fn wrld))))
        (& nil)))))

Theorem: booleanp-of-atc-stmt-noncval-termp

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