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