		Search-engine friendly clone of the ACL2 documentation.

Specialize-implementation

Specialize-ext-declon

Transform an external declaration.

Signature
(specialize-ext-declon extdecl target-fn target-param const) → (mv found new-extdecl)
Arguments: extdecl — Guard (ext-declonp extdecl).; target-fn — Guard (identp target-fn).; target-param — Guard (identp target-param).; const — Guard (exprp const).
Returns: found — Type (booleanp found).; new-extdecl — Type (ext-declonp new-extdecl).

Definitions and Theorems

Function: specialize-ext-declon

(defun specialize-ext-declon (extdecl target-fn target-param const)
  (declare (xargs :guard (and (ext-declonp extdecl)
                              (identp target-fn)
                              (identp target-param)
                              (exprp const))))
  (ext-declon-case
       extdecl :fundef
       (b* (((mv found fundef)
             (specialize-fundef extdecl.fundef
                                target-fn target-param const)))
         (mv found (ext-declon-fundef fundef)))
       :declon (mv nil (ext-declon-fix extdecl))
       :empty (mv nil (ext-declon-fix extdecl))
       :asm (mv nil (ext-declon-fix extdecl))))

Theorem: booleanp-of-specialize-ext-declon.found

(defthm booleanp-of-specialize-ext-declon.found
  (b*
    (((mv ?found ?new-extdecl)
      (specialize-ext-declon extdecl target-fn target-param const)))
    (booleanp found))
  :rule-classes :rewrite)

Theorem: ext-declonp-of-specialize-ext-declon.new-extdecl

(defthm ext-declonp-of-specialize-ext-declon.new-extdecl
  (b*
    (((mv ?found ?new-extdecl)
      (specialize-ext-declon extdecl target-fn target-param const)))
    (ext-declonp new-extdecl))
  :rule-classes :rewrite)