		Search-engine friendly clone of the ACL2 documentation.

Ctxexprs

Vl-modinstlist-ctxexprs

Collect up a vl-ctxexprlist-p from a list of vl-modinstlist-ps.

Signature
(vl-modinstlist-ctxexprs x mod ss) → alist
Arguments: x — Guard (vl-modinstlist-p x).; mod — Guard (stringp mod).; ss — Guard (vl-scopestack-p ss).
Returns: alist — Type (vl-ctxexprlist-p alist).

Definitions and Theorems

Function: vl-modinstlist-ctxexprs

(defun vl-modinstlist-ctxexprs (x mod ss)
  (declare (xargs :guard (and (vl-modinstlist-p x)
                              (stringp mod)
                              (vl-scopestack-p ss))))
  (let ((__function__ 'vl-modinstlist-ctxexprs))
    (declare (ignorable __function__))
    (mbe :logic
         (if (atom x)
             nil
           (append (vl-modinst-ctxexprs (car x) mod ss)
                   (vl-modinstlist-ctxexprs (cdr x)
                                            mod ss)))
         :exec
         (if (atom x)
             nil
           (with-local-nrev
                (vl-modinstlist-ctxexprs-nrev x mod ss nrev))))))

Theorem: vl-ctxexprlist-p-of-vl-modinstlist-ctxexprs

(defthm vl-ctxexprlist-p-of-vl-modinstlist-ctxexprs
  (b* ((alist (vl-modinstlist-ctxexprs x mod ss)))
    (vl-ctxexprlist-p alist))
  :rule-classes :rewrite)

Theorem: vl-modinstlist-ctxexprs-nrev-removal

(defthm vl-modinstlist-ctxexprs-nrev-removal
  (equal (vl-modinstlist-ctxexprs-nrev x mod ss nrev)
         (append nrev
                 (vl-modinstlist-ctxexprs x mod ss))))

Theorem: vl-modinstlist-ctxexprs-of-vl-modinstlist-fix-x

(defthm vl-modinstlist-ctxexprs-of-vl-modinstlist-fix-x
  (equal (vl-modinstlist-ctxexprs (vl-modinstlist-fix x)
                                  mod ss)
         (vl-modinstlist-ctxexprs x mod ss)))

Theorem: vl-modinstlist-ctxexprs-vl-modinstlist-equiv-congruence-on-x

(defthm vl-modinstlist-ctxexprs-vl-modinstlist-equiv-congruence-on-x
  (implies (vl-modinstlist-equiv x x-equiv)
           (equal (vl-modinstlist-ctxexprs x mod ss)
                  (vl-modinstlist-ctxexprs x-equiv mod ss)))
  :rule-classes :congruence)

Theorem: vl-modinstlist-ctxexprs-of-str-fix-mod

(defthm vl-modinstlist-ctxexprs-of-str-fix-mod
  (equal (vl-modinstlist-ctxexprs x (str-fix mod)
                                  ss)
         (vl-modinstlist-ctxexprs x mod ss)))

Theorem: vl-modinstlist-ctxexprs-streqv-congruence-on-mod

(defthm vl-modinstlist-ctxexprs-streqv-congruence-on-mod
  (implies (streqv mod mod-equiv)
           (equal (vl-modinstlist-ctxexprs x mod ss)
                  (vl-modinstlist-ctxexprs x mod-equiv ss)))
  :rule-classes :congruence)

Theorem: vl-modinstlist-ctxexprs-of-vl-scopestack-fix-ss

(defthm vl-modinstlist-ctxexprs-of-vl-scopestack-fix-ss
  (equal (vl-modinstlist-ctxexprs x mod (vl-scopestack-fix ss))
         (vl-modinstlist-ctxexprs x mod ss)))

Theorem: vl-modinstlist-ctxexprs-vl-scopestack-equiv-congruence-on-ss

(defthm vl-modinstlist-ctxexprs-vl-scopestack-equiv-congruence-on-ss
  (implies (vl-scopestack-equiv ss ss-equiv)
           (equal (vl-modinstlist-ctxexprs x mod ss)
                  (vl-modinstlist-ctxexprs x mod ss-equiv)))
  :rule-classes :congruence)

Subtopics

Vl-modinstlist-ctxexprs-nrev