		Search-engine friendly clone of the ACL2 documentation.

Split-fn

Paramdecl-to-ident-paramdecl-map

Convert a parameter declaration into a singleton omap associating the declared identifier to the declaration.

Signature
(paramdecl-to-ident-paramdecl-map paramdecl) → map
Arguments: paramdecl — Guard (paramdeclp paramdecl).
Returns: map — Type (ident-paramdecl-mapp map).

If the parameter declaration is unnamed, or if it has not been disambiguated, the empty map is returned instead.

Definitions and Theorems

Function: paramdecl-to-ident-paramdecl-map

(defun paramdecl-to-ident-paramdecl-map (paramdecl)
 (declare (xargs :guard (paramdeclp paramdecl)))
 (let ((__function__ 'paramdecl-to-ident-paramdecl-map))
  (declare (ignorable __function__))
  (b* (((paramdecl paramdecl) paramdecl))
    (paramdeclor-case
         paramdecl.decl
         :declor (omap::update (declor->ident paramdecl.decl.unwrap)
                               (paramdecl-fix paramdecl)
                               nil)
         :otherwise nil))))

Theorem: ident-paramdecl-mapp-of-paramdecl-to-ident-paramdecl-map

(defthm ident-paramdecl-mapp-of-paramdecl-to-ident-paramdecl-map
  (b* ((map (paramdecl-to-ident-paramdecl-map paramdecl)))
    (ident-paramdecl-mapp map))
  :rule-classes :rewrite)