		Search-engine friendly clone of the ACL2 documentation.

Constant-propagation

Const-prop-extdecl-list

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

Definitions and Theorems

Function: const-prop-extdecl-list

(defun const-prop-extdecl-list (extdecls env)
  (declare (xargs :guard (and (extdecl-listp extdecls)
                              (envp env))))
  (let ((__function__ 'const-prop-extdecl-list))
    (declare (ignorable __function__))
    (if (endp extdecls)
        nil
      (cons (const-prop-extdecl (first extdecls)
                                env)
            (const-prop-extdecl-list (rest extdecls)
                                     env)))))

Theorem: extdecl-listp-of-const-prop-extdecl-list

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