		Search-engine friendly clone of the ACL2 documentation.

Constant-propagation

Const-prop-extdecl

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

Definitions and Theorems

Function: const-prop-extdecl

(defun const-prop-extdecl (extdecl env)
  (declare (xargs :guard (and (extdeclp extdecl) (envp env))))
  (let ((__function__ 'const-prop-extdecl))
    (declare (ignorable __function__))
    (extdecl-case
         extdecl :fundef
         (extdecl-fundef (const-prop-fundef extdecl.unwrap env))
         :decl
         (b* (((mv unwrap -)
               (const-prop-decl extdecl.unwrap env)))
           (extdecl-decl unwrap))
         :empty (extdecl-empty)
         :asm (extdecl-fix extdecl))))

Theorem: extdeclp-of-const-prop-extdecl

(defthm extdeclp-of-const-prop-extdecl
  (b* ((new-extdecl (const-prop-extdecl extdecl env)))
    (extdeclp new-extdecl))
  :rule-classes :rewrite)