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