		Search-engine friendly clone of the ACL2 documentation.

Constant-propagation

Const-prop-ext-declon-list

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

Definitions and Theorems

Function: const-prop-ext-declon-list

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

Theorem: ext-declon-listp-of-const-prop-ext-declon-list

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