		Search-engine friendly clone of the ACL2 documentation.

Eval-state-trans

Eval-state-trans->stack

Get the stack field from a eval-state-trans.

Signature
(eval-state-trans->stack x) → stack
Arguments: x — Guard (eval-state-p x).
Returns: stack — Type (stackp stack).

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

Definitions and Theorems

Function: eval-state-trans->stack$inline

(defun eval-state-trans->stack$inline (x)
  (declare (xargs :guard (eval-state-p x)))
  (declare (xargs :guard (equal (eval-state-kind x) :trans)))
  (let ((__function__ 'eval-state-trans->stack))
    (declare (ignorable __function__))
    (mbe :logic
         (b* ((x (and (equal (eval-state-kind x) :trans)
                      x)))
           (stack-fix (std::da-nth 0 (cdr x))))
         :exec (std::da-nth 0 (cdr x)))))

Theorem: stackp-of-eval-state-trans->stack

(defthm stackp-of-eval-state-trans->stack
  (b* ((stack (eval-state-trans->stack$inline x)))
    (stackp stack))
  :rule-classes :rewrite)

Theorem: eval-state-trans->stack$inline-of-eval-state-fix-x

(defthm eval-state-trans->stack$inline-of-eval-state-fix-x
  (equal (eval-state-trans->stack$inline (eval-state-fix x))
         (eval-state-trans->stack$inline x)))

Theorem: eval-state-trans->stack$inline-eval-state-equiv-congruence-on-x

(defthm
    eval-state-trans->stack$inline-eval-state-equiv-congruence-on-x
  (implies (eval-state-equiv x x-equiv)
           (equal (eval-state-trans->stack$inline x)
                  (eval-state-trans->stack$inline x-equiv)))
  :rule-classes :congruence)

Theorem: eval-state-trans->stack-when-wrong-kind

(defthm eval-state-trans->stack-when-wrong-kind
  (implies (not (equal (eval-state-kind x) :trans))
           (equal (eval-state-trans->stack x)
                  (stack-fix nil))))