		Search-engine friendly clone of the ACL2 documentation.

Lucid

Vl-lucid-ctx

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

Definitions and Theorems

Function: vl-lucid-ctx

(defun vl-lucid-ctx (ss elem)
  (declare (xargs :guard (and (vl-scopestack-p ss)
                              (vl-ctxelement-p elem))))
  (let ((__function__ 'vl-lucid-ctx))
    (declare (ignorable __function__))
    (make-vl-context1 :mod (vl-scopestack->path ss)
                      :elem elem)))

Theorem: vl-context1-p-of-vl-lucid-ctx

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

Theorem: vl-lucid-ctx-of-vl-scopestack-fix-ss

(defthm vl-lucid-ctx-of-vl-scopestack-fix-ss
  (equal (vl-lucid-ctx (vl-scopestack-fix ss)
                       elem)
         (vl-lucid-ctx ss elem)))

Theorem: vl-lucid-ctx-vl-scopestack-equiv-congruence-on-ss

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

Theorem: vl-lucid-ctx-of-vl-ctxelement-fix-elem

(defthm vl-lucid-ctx-of-vl-ctxelement-fix-elem
  (equal (vl-lucid-ctx ss (vl-ctxelement-fix elem))
         (vl-lucid-ctx ss elem)))

Theorem: vl-lucid-ctx-vl-ctxelement-equiv-congruence-on-elem

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