		Search-engine friendly clone of the ACL2 documentation.

Atc-context

Atc-context->preamble

Get the preamble field from a atc-context.

Signature
(atc-context->preamble x) → preamble
Arguments: x — Guard (atc-contextp x).
Returns: preamble — Type (true-listp preamble).

This is an ordinary field accessor created by fty::defprod.

Definitions and Theorems

Function: atc-context->preamble$inline

(defun atc-context->preamble$inline (x)
  (declare (xargs :guard (atc-contextp x)))
  (declare (xargs :guard t))
  (let ((__function__ 'atc-context->preamble))
    (declare (ignorable __function__))
    (mbe :logic
         (b* ((x (and t x)))
           (list-fix (cdr (std::da-nth 0 x))))
         :exec (cdr (std::da-nth 0 x)))))

Theorem: true-listp-of-atc-context->preamble

(defthm true-listp-of-atc-context->preamble
  (b* ((preamble (atc-context->preamble$inline x)))
    (true-listp preamble))
  :rule-classes :rewrite)

Theorem: atc-context->preamble$inline-of-atc-context-fix-x

(defthm atc-context->preamble$inline-of-atc-context-fix-x
  (equal (atc-context->preamble$inline (atc-context-fix x))
         (atc-context->preamble$inline x)))

Theorem: atc-context->preamble$inline-atc-context-equiv-congruence-on-x

(defthm
     atc-context->preamble$inline-atc-context-equiv-congruence-on-x
  (implies (atc-context-equiv x x-equiv)
           (equal (atc-context->preamble$inline x)
                  (atc-context->preamble$inline x-equiv)))
  :rule-classes :congruence)