		Search-engine friendly clone of the ACL2 documentation.

Specialize

Paramdecl-to-decl

Convert a parameter declaration to a regular declaration.

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

Definitions and Theorems

Function: paramdecl-to-decl

(defun paramdecl-to-decl (paramdecl init?)
 (declare (xargs :guard (and (paramdeclp paramdecl)
                             (initer-optionp init?))))
 (let ((__function__ 'paramdecl-to-decl))
  (declare (ignorable __function__))
  (b* (((paramdecl paramdecl) paramdecl))
   (paramdeclor-case
    paramdecl.decl
    :declor
    (mv
     t
     (make-decl-decl
        :extension nil
        :specs paramdecl.spec
        :init (cons (initdeclor paramdecl.decl.unwrap nil nil init?)
                    nil)))
    :otherwise (mv nil (c$::irr-decl))))))

Theorem: booleanp-of-paramdecl-to-decl.success

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

Theorem: declp-of-paramdecl-to-decl.decl

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