(decl-to-ident-paramdecl-map0 declspecs initdeclors) → map
Function:
(defun decl-to-ident-paramdecl-map0 (declspecs initdeclors) (declare (xargs :guard (and (declspec-listp declspecs) (initdeclor-listp initdeclors)))) (let ((__function__ 'decl-to-ident-paramdecl-map0)) (declare (ignorable __function__)) (b* (((when (endp initdeclors)) nil) ((initdeclor initdeclor) (first initdeclors)) (ident? (declor-get-ident initdeclor.declor))) (if ident? (omap::update ident? (make-paramdecl :spec declspecs :decl (paramdeclor-declor initdeclor.declor)) (decl-to-ident-paramdecl-map0 declspecs (rest initdeclors))) (decl-to-ident-paramdecl-map0 declspecs (rest initdeclors))))))
Theorem:
(defthm ident-paramdecl-mapp-of-decl-to-ident-paramdecl-map0 (b* ((map (decl-to-ident-paramdecl-map0 declspecs initdeclors))) (ident-paramdecl-mapp map)) :rule-classes :rewrite)