		Search-engine friendly clone of the ACL2 documentation.

Unparameterization

Vl-gencase-some-match

Signature
(vl-gencase-some-match x y ss scopes warnings) → (mv errmsg warnings equalp)
Arguments: x — Guard (vl-expr-p x).; y — Guard (vl-exprlist-p y).; ss — Guard (vl-scopestack-p ss).; scopes — Guard (vl-elabscopes-p scopes).; warnings — Guard (vl-warninglist-p warnings).
Returns: errmsg — Type (iff (vl-msg-p errmsg) errmsg).; warnings — Type (vl-warninglist-p warnings).

Definitions and Theorems

Function: vl-gencase-some-match

(defun vl-gencase-some-match (x y ss scopes warnings)
  (declare (xargs :guard (and (vl-expr-p x)
                              (vl-exprlist-p y)
                              (vl-scopestack-p ss)
                              (vl-elabscopes-p scopes)
                              (vl-warninglist-p warnings))))
  (let ((__function__ 'vl-gencase-some-match))
    (declare (ignorable __function__))
    (b* (((when (atom y)) (mv nil (ok) nil))
         ((mv errmsg warnings first)
          (vl-gencase-match x (car y)
                            ss scopes warnings))
         ((when errmsg) (mv errmsg warnings nil))
         ((when first) (mv nil warnings first)))
      (vl-gencase-some-match x (cdr y)
                             ss scopes warnings))))

Theorem: return-type-of-vl-gencase-some-match.errmsg

(defthm return-type-of-vl-gencase-some-match.errmsg
  (b* (((mv ?errmsg ?warnings common-lisp::?equalp)
        (vl-gencase-some-match x y ss scopes warnings)))
    (iff (vl-msg-p errmsg) errmsg))
  :rule-classes :rewrite)

Theorem: vl-warninglist-p-of-vl-gencase-some-match.warnings

(defthm vl-warninglist-p-of-vl-gencase-some-match.warnings
  (b* (((mv ?errmsg ?warnings common-lisp::?equalp)
        (vl-gencase-some-match x y ss scopes warnings)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: vl-gencase-some-match-of-vl-expr-fix-x

(defthm vl-gencase-some-match-of-vl-expr-fix-x
  (equal (vl-gencase-some-match (vl-expr-fix x)
                                y ss scopes warnings)
         (vl-gencase-some-match x y ss scopes warnings)))

Theorem: vl-gencase-some-match-vl-expr-equiv-congruence-on-x

(defthm vl-gencase-some-match-vl-expr-equiv-congruence-on-x
  (implies
       (vl-expr-equiv x x-equiv)
       (equal (vl-gencase-some-match x y ss scopes warnings)
              (vl-gencase-some-match x-equiv y ss scopes warnings)))
  :rule-classes :congruence)

Theorem: vl-gencase-some-match-of-vl-exprlist-fix-y

(defthm vl-gencase-some-match-of-vl-exprlist-fix-y
  (equal (vl-gencase-some-match x (vl-exprlist-fix y)
                                ss scopes warnings)
         (vl-gencase-some-match x y ss scopes warnings)))

Theorem: vl-gencase-some-match-vl-exprlist-equiv-congruence-on-y

(defthm vl-gencase-some-match-vl-exprlist-equiv-congruence-on-y
  (implies
       (vl-exprlist-equiv y y-equiv)
       (equal (vl-gencase-some-match x y ss scopes warnings)
              (vl-gencase-some-match x y-equiv ss scopes warnings)))
  :rule-classes :congruence)

Theorem: vl-gencase-some-match-of-vl-scopestack-fix-ss

(defthm vl-gencase-some-match-of-vl-scopestack-fix-ss
  (equal (vl-gencase-some-match x y (vl-scopestack-fix ss)
                                scopes warnings)
         (vl-gencase-some-match x y ss scopes warnings)))

Theorem: vl-gencase-some-match-vl-scopestack-equiv-congruence-on-ss

(defthm vl-gencase-some-match-vl-scopestack-equiv-congruence-on-ss
  (implies
       (vl-scopestack-equiv ss ss-equiv)
       (equal (vl-gencase-some-match x y ss scopes warnings)
              (vl-gencase-some-match x y ss-equiv scopes warnings)))
  :rule-classes :congruence)

Theorem: vl-gencase-some-match-of-vl-elabscopes-fix-scopes

(defthm vl-gencase-some-match-of-vl-elabscopes-fix-scopes
  (equal (vl-gencase-some-match x y ss (vl-elabscopes-fix scopes)
                                warnings)
         (vl-gencase-some-match x y ss scopes warnings)))

Theorem: vl-gencase-some-match-vl-elabscopes-equiv-congruence-on-scopes

(defthm
     vl-gencase-some-match-vl-elabscopes-equiv-congruence-on-scopes
  (implies
       (vl-elabscopes-equiv scopes scopes-equiv)
       (equal (vl-gencase-some-match x y ss scopes warnings)
              (vl-gencase-some-match x y ss scopes-equiv warnings)))
  :rule-classes :congruence)

Theorem: vl-gencase-some-match-of-vl-warninglist-fix-warnings

(defthm vl-gencase-some-match-of-vl-warninglist-fix-warnings
 (equal
     (vl-gencase-some-match x y
                            ss scopes (vl-warninglist-fix warnings))
     (vl-gencase-some-match x y ss scopes warnings)))

Theorem: vl-gencase-some-match-vl-warninglist-equiv-congruence-on-warnings

(defthm
  vl-gencase-some-match-vl-warninglist-equiv-congruence-on-warnings
  (implies
       (vl-warninglist-equiv warnings warnings-equiv)
       (equal (vl-gencase-some-match x y ss scopes warnings)
              (vl-gencase-some-match x y ss scopes warnings-equiv)))
  :rule-classes :congruence)