		Search-engine friendly clone of the ACL2 documentation.

Ctxexprs

Vl-exprlist-ctxexprs

Bind some expressions to their context.

Signature
(vl-exprlist-ctxexprs exprs ctx ss) → ctxexprs
Arguments: exprs — List of expressions to bind.
Guard (vl-exprlist-p exprs).; ctx — Context to bind to all of these expressions.
Guard (vl-context1-p ctx).; ss — Scopestack to bind them all to.
Guard (vl-scopestack-p ss).
Returns: ctxexprs — Type (vl-ctxexprlist-p ctxexprs).

Definitions and Theorems

Function: vl-exprlist-ctxexprs

(defun vl-exprlist-ctxexprs (exprs ctx ss)
  (declare (xargs :guard (and (vl-exprlist-p exprs)
                              (vl-context1-p ctx)
                              (vl-scopestack-p ss))))
  (let ((__function__ 'vl-exprlist-ctxexprs))
    (declare (ignorable __function__))
    (mbe :logic
         (if (atom exprs)
             nil
           (cons (make-vl-ctxexpr :expr (car exprs)
                                  :ctx ctx
                                  :ss ss)
                 (vl-exprlist-ctxexprs (cdr exprs)
                                       ctx ss)))
         :exec
         (if (atom exprs)
             nil
           (with-local-nrev
                (vl-exprlist-ctxexprs-nrev exprs ctx ss nrev))))))

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

(defthm vl-ctxexprlist-p-of-vl-exprlist-ctxexprs
  (b* ((ctxexprs (vl-exprlist-ctxexprs exprs ctx ss)))
    (vl-ctxexprlist-p ctxexprs))
  :rule-classes :rewrite)

Theorem: vl-exprlist-ctxexprs-nrev-removal

(defthm vl-exprlist-ctxexprs-nrev-removal
  (equal (vl-exprlist-ctxexprs-nrev exprs ctx ss nrev)
         (append nrev
                 (vl-exprlist-ctxexprs exprs ctx ss))))

Theorem: vl-exprlist-ctxexprs-of-vl-exprlist-fix-exprs

(defthm vl-exprlist-ctxexprs-of-vl-exprlist-fix-exprs
  (equal (vl-exprlist-ctxexprs (vl-exprlist-fix exprs)
                               ctx ss)
         (vl-exprlist-ctxexprs exprs ctx ss)))

Theorem: vl-exprlist-ctxexprs-vl-exprlist-equiv-congruence-on-exprs

(defthm vl-exprlist-ctxexprs-vl-exprlist-equiv-congruence-on-exprs
  (implies (vl-exprlist-equiv exprs exprs-equiv)
           (equal (vl-exprlist-ctxexprs exprs ctx ss)
                  (vl-exprlist-ctxexprs exprs-equiv ctx ss)))
  :rule-classes :congruence)

Theorem: vl-exprlist-ctxexprs-of-vl-context1-fix-ctx

(defthm vl-exprlist-ctxexprs-of-vl-context1-fix-ctx
  (equal (vl-exprlist-ctxexprs exprs (vl-context1-fix ctx)
                               ss)
         (vl-exprlist-ctxexprs exprs ctx ss)))

Theorem: vl-exprlist-ctxexprs-vl-context1-equiv-congruence-on-ctx

(defthm vl-exprlist-ctxexprs-vl-context1-equiv-congruence-on-ctx
  (implies (vl-context1-equiv ctx ctx-equiv)
           (equal (vl-exprlist-ctxexprs exprs ctx ss)
                  (vl-exprlist-ctxexprs exprs ctx-equiv ss)))
  :rule-classes :congruence)

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

(defthm vl-exprlist-ctxexprs-of-vl-scopestack-fix-ss
  (equal (vl-exprlist-ctxexprs exprs ctx (vl-scopestack-fix ss))
         (vl-exprlist-ctxexprs exprs ctx ss)))

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

(defthm vl-exprlist-ctxexprs-vl-scopestack-equiv-congruence-on-ss
  (implies (vl-scopestack-equiv ss ss-equiv)
           (equal (vl-exprlist-ctxexprs exprs ctx ss)
                  (vl-exprlist-ctxexprs exprs ctx ss-equiv)))
  :rule-classes :congruence)

Subtopics

Vl-exprlist-ctxexprs-nrev