(vl-exprlist-ctxexprs-nrev exprs ctx ss nrev) → nrev
Function:
(defun vl-exprlist-ctxexprs-nrev (exprs ctx ss nrev) (declare (xargs :stobjs (nrev))) (declare (xargs :guard (and (vl-exprlist-p exprs) (vl-context1-p ctx) (vl-scopestack-p ss)))) (let ((__function__ 'vl-exprlist-ctxexprs-nrev)) (declare (ignorable __function__)) (if (atom exprs) (nrev-fix nrev) (let ((nrev (nrev-push (make-vl-ctxexpr :expr (car exprs) :ctx ctx :ss ss) nrev))) (vl-exprlist-ctxexprs-nrev (cdr exprs) ctx ss nrev)))))
Theorem:
(defthm vl-exprlist-ctxexprs-nrev-of-vl-exprlist-fix-exprs (equal (vl-exprlist-ctxexprs-nrev (vl-exprlist-fix exprs) ctx ss nrev) (vl-exprlist-ctxexprs-nrev exprs ctx ss nrev)))
Theorem:
(defthm vl-exprlist-ctxexprs-nrev-vl-exprlist-equiv-congruence-on-exprs (implies (vl-exprlist-equiv exprs exprs-equiv) (equal (vl-exprlist-ctxexprs-nrev exprs ctx ss nrev) (vl-exprlist-ctxexprs-nrev exprs-equiv ctx ss nrev))) :rule-classes :congruence)
Theorem:
(defthm vl-exprlist-ctxexprs-nrev-of-vl-context1-fix-ctx (equal (vl-exprlist-ctxexprs-nrev exprs (vl-context1-fix ctx) ss nrev) (vl-exprlist-ctxexprs-nrev exprs ctx ss nrev)))
Theorem:
(defthm vl-exprlist-ctxexprs-nrev-vl-context1-equiv-congruence-on-ctx (implies (vl-context1-equiv ctx ctx-equiv) (equal (vl-exprlist-ctxexprs-nrev exprs ctx ss nrev) (vl-exprlist-ctxexprs-nrev exprs ctx-equiv ss nrev))) :rule-classes :congruence)
Theorem:
(defthm vl-exprlist-ctxexprs-nrev-of-vl-scopestack-fix-ss (equal (vl-exprlist-ctxexprs-nrev exprs ctx (vl-scopestack-fix ss) nrev) (vl-exprlist-ctxexprs-nrev exprs ctx ss nrev)))
Theorem:
(defthm vl-exprlist-ctxexprs-nrev-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-exprlist-ctxexprs-nrev exprs ctx ss nrev) (vl-exprlist-ctxexprs-nrev exprs ctx ss-equiv nrev))) :rule-classes :congruence)