		Search-engine friendly clone of the ACL2 documentation.

Vl-lucidstate

Vl-lucidocc->ctx

Signature
(vl-lucidocc->ctx x) → ctx
Arguments: x — Guard (vl-lucidocc-p x).
Returns: ctx — Type (vl-lucidctx-p ctx).

Definitions and Theorems

Function: vl-lucidocc->ctx$inline

(defun vl-lucidocc->ctx$inline (x)
  (declare (xargs :guard (vl-lucidocc-p x)))
  (let ((__function__ 'vl-lucidocc->ctx))
    (declare (ignorable __function__))
    (vl-lucidocc-case x
                      :solo x.ctx
                      :slice x.ctx
                      :tail x.ctx)))

Theorem: vl-lucidctx-p-of-vl-lucidocc->ctx

(defthm vl-lucidctx-p-of-vl-lucidocc->ctx
  (b* ((ctx (vl-lucidocc->ctx$inline x)))
    (vl-lucidctx-p ctx))
  :rule-classes :rewrite)

Theorem: vl-lucidocc->ctx$inline-of-vl-lucidocc-fix-x

(defthm vl-lucidocc->ctx$inline-of-vl-lucidocc-fix-x
  (equal (vl-lucidocc->ctx$inline (vl-lucidocc-fix x))
         (vl-lucidocc->ctx$inline x)))

Theorem: vl-lucidocc->ctx$inline-vl-lucidocc-equiv-congruence-on-x

(defthm vl-lucidocc->ctx$inline-vl-lucidocc-equiv-congruence-on-x
  (implies (vl-lucidocc-equiv x x-equiv)
           (equal (vl-lucidocc->ctx$inline x)
                  (vl-lucidocc->ctx$inline x-equiv)))
  :rule-classes :congruence)