		Search-engine friendly clone of the ACL2 documentation.

Leftright-check

Vl-expr-leftright-check

Signature
(vl-expr-leftright-check x ctx) → warnings
Arguments: x — Guard (vl-expr-p x).; ctx — Guard (vl-context1-p ctx).
Returns: warnings — Type (vl-warninglist-p warnings).

Definitions and Theorems

Function: vl-expr-leftright-check

(defun vl-expr-leftright-check (x ctx)
  (declare (xargs :guard (and (vl-expr-p x)
                              (vl-context1-p ctx))))
  (let ((__function__ 'vl-expr-leftright-check))
    (declare (ignorable __function__))
    (vl-expr-leftright-check1 x (vl-expr-indexy-via-ctx x ctx)
                              ctx)))

Theorem: vl-warninglist-p-of-vl-expr-leftright-check

(defthm vl-warninglist-p-of-vl-expr-leftright-check
  (b* ((warnings (vl-expr-leftright-check x ctx)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: vl-expr-leftright-check-of-vl-expr-fix-x

(defthm vl-expr-leftright-check-of-vl-expr-fix-x
  (equal (vl-expr-leftright-check (vl-expr-fix x)
                                  ctx)
         (vl-expr-leftright-check x ctx)))

Theorem: vl-expr-leftright-check-vl-expr-equiv-congruence-on-x

(defthm vl-expr-leftright-check-vl-expr-equiv-congruence-on-x
  (implies (vl-expr-equiv x x-equiv)
           (equal (vl-expr-leftright-check x ctx)
                  (vl-expr-leftright-check x-equiv ctx)))
  :rule-classes :congruence)

Theorem: vl-expr-leftright-check-of-vl-context1-fix-ctx

(defthm vl-expr-leftright-check-of-vl-context1-fix-ctx
  (equal (vl-expr-leftright-check x (vl-context1-fix ctx))
         (vl-expr-leftright-check x ctx)))

Theorem: vl-expr-leftright-check-vl-context1-equiv-congruence-on-ctx

(defthm vl-expr-leftright-check-vl-context1-equiv-congruence-on-ctx
  (implies (vl-context1-equiv ctx ctx-equiv)
           (equal (vl-expr-leftright-check x ctx)
                  (vl-expr-leftright-check x ctx-equiv)))
  :rule-classes :congruence)