		Search-engine friendly clone of the ACL2 documentation.

Atc-context

Atc-contextp

Recognizer for atc-context structures.

Signature
(atc-contextp x) → *

Definitions and Theorems

Function: atc-contextp

(defun atc-contextp (x)
  (declare (xargs :guard t))
  (let ((__function__ 'atc-contextp))
    (declare (ignorable __function__))
    (and (mbe :logic (and (alistp x)
                          (equal (strip-cars x)
                                 '(preamble premises)))
              :exec (fty::alist-with-carsp x '(preamble premises)))
         (b* ((preamble (cdr (std::da-nth 0 x)))
              (premises (cdr (std::da-nth 1 x))))
           (and (true-listp preamble)
                (atc-premise-listp premises))))))

Theorem: consp-when-atc-contextp

(defthm consp-when-atc-contextp
  (implies (atc-contextp x) (consp x))
  :rule-classes :compound-recognizer)