		Search-engine friendly clone of the ACL2 documentation.

Split-fn-implementation

Declon-to-ident-param-declon-map0

Signature
(declon-to-ident-param-declon-map0 declspecs initdeclors) → map
Arguments: declspecs — Guard (decl-spec-listp declspecs).; initdeclors — Guard (init-declor-listp initdeclors).
Returns: map — Type (ident-param-declon-mapp map).

Definitions and Theorems

Function: declon-to-ident-param-declon-map0

(defun declon-to-ident-param-declon-map0 (declspecs initdeclors)
 (declare (xargs :guard (and (decl-spec-listp declspecs)
                             (init-declor-listp initdeclors))))
 (b* (((when (endp initdeclors)) nil)
      ((init-declor initdeclor)
       (first initdeclors))
      (ident (declor->ident initdeclor.declor)))
  (omap::update
   ident
   (make-param-declon
    :specs declspecs
    :declor (make-param-declor-nonabstract :declor initdeclor.declor
                                           :info nil)
    :attribs nil)
   (declon-to-ident-param-declon-map0
        declspecs (rest initdeclors)))))

Theorem: ident-param-declon-mapp-of-declon-to-ident-param-declon-map0

(defthm ident-param-declon-mapp-of-declon-to-ident-param-declon-map0
  (b*
   ((map (declon-to-ident-param-declon-map0 declspecs initdeclors)))
   (ident-param-declon-mapp map))
  :rule-classes :rewrite)