		Search-engine friendly clone of the ACL2 documentation.

Ctxexprs

Vl-make-exprctxalist

Bind some expressions to their context.

Signature
(vl-make-exprctxalist exprs ctx) → alist
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).
Returns: alist — Type (vl-exprctxalist-p alist).

Definitions and Theorems

Function: vl-make-exprctxalist

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

Theorem: vl-exprctxalist-p-of-vl-make-exprctxalist

(defthm vl-exprctxalist-p-of-vl-make-exprctxalist
  (b* ((alist (vl-make-exprctxalist exprs ctx)))
    (vl-exprctxalist-p alist))
  :rule-classes :rewrite)

Theorem: vl-make-exprctxalist-nrev-removal

(defthm vl-make-exprctxalist-nrev-removal
  (equal (vl-make-exprctxalist-nrev exprs ctx nrev)
         (append nrev (vl-make-exprctxalist exprs ctx))))

Theorem: vl-make-exprctxalist-of-vl-exprlist-fix-exprs

(defthm vl-make-exprctxalist-of-vl-exprlist-fix-exprs
  (equal (vl-make-exprctxalist (vl-exprlist-fix exprs)
                               ctx)
         (vl-make-exprctxalist exprs ctx)))

Theorem: vl-make-exprctxalist-vl-exprlist-equiv-congruence-on-exprs

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

Theorem: vl-make-exprctxalist-of-vl-context1-fix-ctx

(defthm vl-make-exprctxalist-of-vl-context1-fix-ctx
  (equal (vl-make-exprctxalist exprs (vl-context1-fix ctx))
         (vl-make-exprctxalist exprs ctx)))

Theorem: vl-make-exprctxalist-vl-context1-equiv-congruence-on-ctx

(defthm vl-make-exprctxalist-vl-context1-equiv-congruence-on-ctx
  (implies (vl-context1-equiv ctx ctx-equiv)
           (equal (vl-make-exprctxalist exprs ctx)
                  (vl-make-exprctxalist exprs ctx-equiv)))
  :rule-classes :congruence)

Subtopics

Vl-make-exprctxalist-nrev