Fold paramdecl-to-ident-paramdecl-map over a list.
(paramdecl-list-to-ident-paramdecl-map paramdecls) → map
Function:
(defun paramdecl-list-to-ident-paramdecl-map (paramdecls) (declare (xargs :guard (paramdecl-listp paramdecls))) (let ((__function__ 'paramdecl-list-to-ident-paramdecl-map)) (declare (ignorable __function__)) (if (endp paramdecls) nil (omap::update* (paramdecl-to-ident-paramdecl-map (first paramdecls)) (paramdecl-list-to-ident-paramdecl-map (rest paramdecls))))))
Theorem:
(defthm ident-paramdecl-mapp-of-paramdecl-list-to-ident-paramdecl-map (b* ((map (paramdecl-list-to-ident-paramdecl-map paramdecls))) (ident-paramdecl-mapp map)) :rule-classes :rewrite)