		Search-engine friendly clone of the ACL2 documentation.

Specialize-implementation

Param-declon-to-decl

Convert a parameter declaration to a regular declaration.

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

Definitions and Theorems

Function: param-declon-to-decl

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

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

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

Theorem: declp-of-param-declon-to-decl.decl

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