		Search-engine friendly clone of the ACL2 documentation.

Specialize

Specialize-extdecl

Transform an external declaration.

Signature
(specialize-extdecl extdecl target-fn target-param const) → (mv found new-extdecl)
Arguments: extdecl — Guard (extdeclp 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 (extdeclp new-extdecl).

Definitions and Theorems

Function: specialize-extdecl

(defun specialize-extdecl (extdecl target-fn target-param const)
  (declare (xargs :guard (and (extdeclp extdecl)
                              (identp target-fn)
                              (identp target-param)
                              (exprp const))))
  (let ((__function__ 'specialize-extdecl))
    (declare (ignorable __function__))
    (extdecl-case
         extdecl :fundef
         (b* (((mv found fundef)
               (specialize-fundef extdecl.unwrap
                                  target-fn target-param const)))
           (mv found (extdecl-fundef fundef)))
         :decl (mv nil (extdecl-fix extdecl))
         :empty (mv nil (extdecl-fix extdecl))
         :asm (mv nil (extdecl-fix extdecl)))))

Theorem: booleanp-of-specialize-extdecl.found

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

Theorem: extdeclp-of-specialize-extdecl.new-extdecl

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