(vl-modinstlist-ppmap x ss item-map &key (ps 'ps)) → (mv item-map ps)
Function:
(defun vl-modinstlist-ppmap-fn (x ss item-map ps) (declare (xargs :stobjs (ps))) (declare (xargs :guard (and (vl-modinstlist-p x) (vl-scopestack-p ss) (vl-commentmap-p item-map)))) (let ((__function__ 'vl-modinstlist-ppmap)) (declare (ignorable __function__)) (b* (((when (atom x)) (mv (vl-commentmap-fix item-map) ps)) ((mv str ps) (with-semilocal-ps (vl-pp-modinst (car x) ss))) (item-map (cons (cons (vl-modinst->loc (car x)) str) item-map))) (vl-modinstlist-ppmap (cdr x) ss item-map))))
Theorem:
(defthm vl-commentmap-p-of-vl-modinstlist-ppmap.item-map (b* (((mv ?item-map ?ps) (vl-modinstlist-ppmap-fn x ss item-map ps))) (vl-commentmap-p item-map)) :rule-classes :rewrite)
Theorem:
(defthm vl-modinstlist-ppmap-fn-of-vl-modinstlist-fix-x (equal (vl-modinstlist-ppmap-fn (vl-modinstlist-fix x) ss item-map ps) (vl-modinstlist-ppmap-fn x ss item-map ps)))
Theorem:
(defthm vl-modinstlist-ppmap-fn-vl-modinstlist-equiv-congruence-on-x (implies (vl-modinstlist-equiv x x-equiv) (equal (vl-modinstlist-ppmap-fn x ss item-map ps) (vl-modinstlist-ppmap-fn x-equiv ss item-map ps))) :rule-classes :congruence)
Theorem:
(defthm vl-modinstlist-ppmap-fn-of-vl-scopestack-fix-ss (equal (vl-modinstlist-ppmap-fn x (vl-scopestack-fix ss) item-map ps) (vl-modinstlist-ppmap-fn x ss item-map ps)))
Theorem:
(defthm vl-modinstlist-ppmap-fn-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-modinstlist-ppmap-fn x ss item-map ps) (vl-modinstlist-ppmap-fn x ss-equiv item-map ps))) :rule-classes :congruence)
Theorem:
(defthm vl-modinstlist-ppmap-fn-of-vl-commentmap-fix-item-map (equal (vl-modinstlist-ppmap-fn x ss (vl-commentmap-fix item-map) ps) (vl-modinstlist-ppmap-fn x ss item-map ps)))
Theorem:
(defthm vl-modinstlist-ppmap-fn-vl-commentmap-equiv-congruence-on-item-map (implies (vl-commentmap-equiv item-map item-map-equiv) (equal (vl-modinstlist-ppmap-fn x ss item-map ps) (vl-modinstlist-ppmap-fn x ss item-map-equiv ps))) :rule-classes :congruence)