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