		Search-engine friendly clone of the ACL2 documentation.

Specialize-implementation

Param-declon-to-declon

Convert a parameter declaration to a regular declaration.

Signature
(param-declon-to-declon paramdecl initer?) → (mv success declon)
Arguments: paramdecl — Guard (param-declonp paramdecl).; initer? — Guard (initer-optionp initer?).
Returns: success — Type (booleanp success).; declon — Type (declonp declon).

Definitions and Theorems

Function: param-declon-to-declon

(defun param-declon-to-declon (paramdecl initer?)
 (declare (xargs :guard (and (param-declonp paramdecl)
                             (initer-optionp initer?))))
 (b* (((param-declon paramdecl) paramdecl))
   (param-declor-case
        paramdecl.declor
        :nonabstract
        (mv t
            (make-declon-declon
                 :extension nil
                 :specs paramdecl.specs
                 :declors (list (init-declor paramdecl.declor.declor
                                             nil nil initer? nil))))
        :otherwise (mv nil (irr-declon)))))

Theorem: booleanp-of-param-declon-to-declon.success

(defthm booleanp-of-param-declon-to-declon.success
  (b* (((mv ?success c$::?declon)
        (param-declon-to-declon paramdecl initer?)))
    (booleanp success))
  :rule-classes :rewrite)

Theorem: declonp-of-param-declon-to-declon.declon

(defthm declonp-of-param-declon-to-declon.declon
  (b* (((mv ?success c$::?declon)
        (param-declon-to-declon paramdecl initer?)))
    (declonp declon))
  :rule-classes :rewrite)