		Search-engine friendly clone of the ACL2 documentation.

Split-fn

Decl-to-ident-paramdecl-map0

Signature
(decl-to-ident-paramdecl-map0 declspecs initdeclors) → map
Arguments: declspecs — Guard (decl-spec-listp declspecs).; initdeclors — Guard (initdeclor-listp initdeclors).
Returns: map — Type (ident-paramdecl-mapp map).

Definitions and Theorems

Function: decl-to-ident-paramdecl-map0

(defun decl-to-ident-paramdecl-map0 (declspecs initdeclors)
 (declare (xargs :guard (and (decl-spec-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->ident initdeclor.declor)))
   (omap::update
     ident
     (make-paramdecl :spec declspecs
                     :decl (paramdeclor-declor initdeclor.declor))
     (decl-to-ident-paramdecl-map0 declspecs (rest initdeclors))))))

Theorem: ident-paramdecl-mapp-of-decl-to-ident-paramdecl-map0

(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)