		Search-engine friendly clone of the ACL2 documentation.

Lucid

Vl-basic-lucidctx

Signature
(vl-basic-lucidctx ss elem) → ctx
Arguments: ss — Guard (vl-scopestack-p ss).; elem — Guard (vl-ctxelement-p elem).
Returns: ctx — Type (vl-lucidctx-p ctx).

Definitions and Theorems

Function: vl-basic-lucidctx

(defun vl-basic-lucidctx (ss elem)
  (declare (xargs :guard (and (vl-scopestack-p ss)
                              (vl-ctxelement-p elem))))
  (let ((__function__ 'vl-basic-lucidctx))
    (declare (ignorable __function__))
    (make-vl-lucidctx :modname (vl-scopestack->path ss)
                      :ss ss
                      :elem elem)))

Theorem: vl-lucidctx-p-of-vl-basic-lucidctx

(defthm vl-lucidctx-p-of-vl-basic-lucidctx
  (b* ((ctx (vl-basic-lucidctx ss elem)))
    (vl-lucidctx-p ctx))
  :rule-classes :rewrite)

Theorem: vl-basic-lucidctx-of-vl-scopestack-fix-ss

(defthm vl-basic-lucidctx-of-vl-scopestack-fix-ss
  (equal (vl-basic-lucidctx (vl-scopestack-fix ss)
                            elem)
         (vl-basic-lucidctx ss elem)))

Theorem: vl-basic-lucidctx-vl-scopestack-equiv-congruence-on-ss

(defthm vl-basic-lucidctx-vl-scopestack-equiv-congruence-on-ss
  (implies (vl-scopestack-equiv ss ss-equiv)
           (equal (vl-basic-lucidctx ss elem)
                  (vl-basic-lucidctx ss-equiv elem)))
  :rule-classes :congruence)

Theorem: vl-basic-lucidctx-of-vl-ctxelement-fix-elem

(defthm vl-basic-lucidctx-of-vl-ctxelement-fix-elem
  (equal (vl-basic-lucidctx ss (vl-ctxelement-fix elem))
         (vl-basic-lucidctx ss elem)))

Theorem: vl-basic-lucidctx-vl-ctxelement-equiv-congruence-on-elem

(defthm vl-basic-lucidctx-vl-ctxelement-equiv-congruence-on-elem
  (implies (vl-ctxelement-equiv elem elem-equiv)
           (equal (vl-basic-lucidctx ss elem)
                  (vl-basic-lucidctx ss elem-equiv)))
  :rule-classes :congruence)