(vl-collect-exprs-for-implicit-wires-from-namedarg x) → (mv main other)
Function:
(defun vl-collect-exprs-for-implicit-wires-from-namedarg (x) (declare (xargs :guard (vl-namedarg-p x))) (let ((__function__ 'vl-collect-exprs-for-implicit-wires-from-namedarg)) (declare (ignorable __function__)) (b* (((vl-namedarg x)) ((when x.nameonly-p) (mv nil (vl-maybe-expr-allexprs x.expr)))) (mv (vl-maybe-expr-allexprs x.expr) nil))))
Theorem:
(defthm vl-exprlist-p-of-vl-collect-exprs-for-implicit-wires-from-namedarg.main (b* (((mv ?main ?other) (vl-collect-exprs-for-implicit-wires-from-namedarg x))) (vl-exprlist-p main)) :rule-classes :rewrite)
Theorem:
(defthm vl-exprlist-p-of-vl-collect-exprs-for-implicit-wires-from-namedarg.other (b* (((mv ?main ?other) (vl-collect-exprs-for-implicit-wires-from-namedarg x))) (vl-exprlist-p other)) :rule-classes :rewrite)
Theorem:
(defthm vl-collect-exprs-for-implicit-wires-from-namedarg-mvtypes-0 (true-listp (mv-nth 0 (vl-collect-exprs-for-implicit-wires-from-namedarg x))) :rule-classes :type-prescription)
Theorem:
(defthm vl-collect-exprs-for-implicit-wires-from-namedarg-mvtypes-1 (true-listp (mv-nth 1 (vl-collect-exprs-for-implicit-wires-from-namedarg x))) :rule-classes :type-prescription)
Theorem:
(defthm vl-collect-exprs-for-implicit-wires-from-namedarg-complete (b* (((mv main other) (vl-collect-exprs-for-implicit-wires-from-namedarg x))) (set-equiv (append main other) (vl-namedarg-allexprs x))))
Theorem:
(defthm vl-collect-exprs-for-implicit-wires-from-namedarg-of-vl-namedarg-fix-x (equal (vl-collect-exprs-for-implicit-wires-from-namedarg (vl-namedarg-fix x)) (vl-collect-exprs-for-implicit-wires-from-namedarg x)))
Theorem:
(defthm vl-collect-exprs-for-implicit-wires-from-namedarg-vl-namedarg-equiv-congruence-on-x (implies (vl-namedarg-equiv x x-equiv) (equal (vl-collect-exprs-for-implicit-wires-from-namedarg x) (vl-collect-exprs-for-implicit-wires-from-namedarg x-equiv))) :rule-classes :congruence)