		Search-engine friendly clone of the ACL2 documentation.

Constant-propagation

Const-prop-ext-declon

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

Definitions and Theorems

Function: const-prop-ext-declon

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

Theorem: ext-declonp-of-const-prop-ext-declon

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