		Search-engine friendly clone of the ACL2 documentation.

Constant-propagation

Const-prop-fundef

Signature
(const-prop-fundef fundef env) → new-fundef
Arguments: fundef — Guard (fundefp fundef).; env — Guard (envp env).
Returns: new-fundef — Type (fundefp new-fundef).

Definitions and Theorems

Function: const-prop-fundef

(defun const-prop-fundef (fundef env)
  (declare (xargs :guard (and (fundefp fundef) (envp env))))
  (let ((__function__ 'const-prop-fundef))
    (declare (ignorable __function__))
    (b* (((fundef fundef) fundef)
         ((mv spec -)
          (const-prop-decl-spec-list fundef.spec env))
         ((mv declor -)
          (const-prop-declor fundef.declor env))
         ((mv decls -)
          (const-prop-decl-list fundef.decls env))
         ((mv body -)
          (const-prop-stmt fundef.body (push-scope-env env))))
      (make-fundef :extension fundef.extension
                   :spec spec
                   :declor declor
                   :asm? fundef.asm?
                   :decls decls
                   :body body))))

Theorem: fundefp-of-const-prop-fundef

(defthm fundefp-of-const-prop-fundef
  (b* ((new-fundef (const-prop-fundef fundef env)))
    (fundefp new-fundef))
  :rule-classes :rewrite)