		Search-engine friendly clone of the ACL2 documentation.

Unparameterization

Vl-packagelist-elaborate

Signature
(vl-packagelist-elaborate x elabindex warnings &key (config 'config)) → (mv ok warnings1 new-elabindex new-x)
Arguments: x — Guard (vl-packagelist-p x).; elabindex — design level.; warnings — Guard (vl-warninglist-p warnings).; config — Guard (vl-simpconfig-p config).
Returns: warnings1 — Type (vl-warninglist-p warnings1).; new-x — Type (vl-packagelist-p new-x).

Definitions and Theorems

Function: vl-packagelist-elaborate-fn

(defun vl-packagelist-elaborate-fn (x elabindex warnings config)
  (declare (xargs :stobjs (elabindex)))
  (declare (xargs :guard (and (vl-packagelist-p x)
                              (vl-warninglist-p warnings)
                              (vl-simpconfig-p config))))
  (let ((__function__ 'vl-packagelist-elaborate))
    (declare (ignorable __function__))
    (b* (((when (atom x))
          (mv t (ok) elabindex nil))
         ((mv ok1 warnings elabindex pkg1)
          (vl-package-elaborate (car x)
                                elabindex warnings))
         ((mv ok2 warnings elabindex pkgs)
          (vl-packagelist-elaborate (cdr x)
                                    elabindex warnings)))
      (mv (and ok1 ok2)
          warnings elabindex (cons pkg1 pkgs)))))

Theorem: vl-warninglist-p-of-vl-packagelist-elaborate.warnings1

(defthm vl-warninglist-p-of-vl-packagelist-elaborate.warnings1
  (b* (((mv ?ok ?warnings1 ?new-elabindex ?new-x)
        (vl-packagelist-elaborate-fn x elabindex warnings config)))
    (vl-warninglist-p warnings1))
  :rule-classes :rewrite)

Theorem: vl-packagelist-p-of-vl-packagelist-elaborate.new-x

(defthm vl-packagelist-p-of-vl-packagelist-elaborate.new-x
  (b* (((mv ?ok ?warnings1 ?new-elabindex ?new-x)
        (vl-packagelist-elaborate-fn x elabindex warnings config)))
    (vl-packagelist-p new-x))
  :rule-classes :rewrite)

Theorem: vl-packagelist-elaborate-fn-of-vl-packagelist-fix-x

(defthm vl-packagelist-elaborate-fn-of-vl-packagelist-fix-x
  (equal (vl-packagelist-elaborate-fn (vl-packagelist-fix x)
                                      elabindex warnings config)
         (vl-packagelist-elaborate-fn x elabindex warnings config)))

Theorem: vl-packagelist-elaborate-fn-vl-packagelist-equiv-congruence-on-x

(defthm
   vl-packagelist-elaborate-fn-vl-packagelist-equiv-congruence-on-x
 (implies
  (vl-packagelist-equiv x x-equiv)
  (equal
   (vl-packagelist-elaborate-fn x elabindex warnings config)
   (vl-packagelist-elaborate-fn x-equiv elabindex warnings config)))
 :rule-classes :congruence)

Theorem: vl-packagelist-elaborate-fn-of-vl-warninglist-fix-warnings

(defthm vl-packagelist-elaborate-fn-of-vl-warninglist-fix-warnings
  (equal (vl-packagelist-elaborate-fn
              x
              elabindex (vl-warninglist-fix warnings)
              config)
         (vl-packagelist-elaborate-fn x elabindex warnings config)))

Theorem: vl-packagelist-elaborate-fn-vl-warninglist-equiv-congruence-on-warnings

(defthm
 vl-packagelist-elaborate-fn-vl-warninglist-equiv-congruence-on-warnings
 (implies
  (vl-warninglist-equiv warnings warnings-equiv)
  (equal
   (vl-packagelist-elaborate-fn x elabindex warnings config)
   (vl-packagelist-elaborate-fn x elabindex warnings-equiv config)))
 :rule-classes :congruence)

Theorem: vl-packagelist-elaborate-fn-of-vl-simpconfig-fix-config

(defthm vl-packagelist-elaborate-fn-of-vl-simpconfig-fix-config
 (equal
   (vl-packagelist-elaborate-fn x elabindex
                                warnings (vl-simpconfig-fix config))
   (vl-packagelist-elaborate-fn x elabindex warnings config)))

Theorem: vl-packagelist-elaborate-fn-vl-simpconfig-equiv-congruence-on-config

(defthm
 vl-packagelist-elaborate-fn-vl-simpconfig-equiv-congruence-on-config
 (implies
  (vl-simpconfig-equiv config config-equiv)
  (equal
   (vl-packagelist-elaborate-fn x elabindex warnings config)
   (vl-packagelist-elaborate-fn x elabindex warnings config-equiv)))
 :rule-classes :congruence)