		Search-engine friendly clone of the ACL2 documentation.

Stmt-gout

Stmt-goutp

Recognizer for stmt-gout structures.

Signature
(stmt-goutp x) → *

Definitions and Theorems

Function: stmt-goutp

(defun stmt-goutp (x)
 (declare (xargs :guard t))
 (let ((__function__ 'stmt-goutp))
  (declare (ignorable __function__))
  (and
     (mbe :logic
          (and (alistp x)
               (equal (strip-cars x)
                      '(items type term context inscope limit events
                              thm-name thm-index names-to-avoid)))
          :exec (fty::alist-with-carsp
                     x
                     '(items type term context inscope limit events
                             thm-name thm-index names-to-avoid)))
     (b* ((items (cdr (std::da-nth 0 x)))
          (type (cdr (std::da-nth 1 x)))
          (term (cdr (std::da-nth 2 x)))
          (context (cdr (std::da-nth 3 x)))
          (inscope (cdr (std::da-nth 4 x)))
          (limit (cdr (std::da-nth 5 x)))
          (events (cdr (std::da-nth 6 x)))
          (thm-name (cdr (std::da-nth 7 x)))
          (thm-index (cdr (std::da-nth 8 x)))
          (names-to-avoid (cdr (std::da-nth 9 x))))
       (and (block-item-listp items)
            (typep type)
            (pseudo-termp term)
            (atc-contextp context)
            (atc-symbol-varinfo-alist-listp inscope)
            (pseudo-termp limit)
            (pseudo-event-form-listp events)
            (symbolp thm-name)
            (posp thm-index)
            (symbol-listp names-to-avoid))))))

Theorem: consp-when-stmt-goutp

(defthm consp-when-stmt-goutp
  (implies (stmt-goutp x) (consp x))
  :rule-classes :compound-recognizer)