		Search-engine friendly clone of the ACL2 documentation.

Simpadd0

Simpadd0-extdecl-list

Transform a list of external declarations.

Signature
(simpadd0-extdecl-list extdecls) → new-extdecls
Arguments: extdecls — Guard (extdecl-listp extdecls).
Returns: new-extdecls — Type (extdecl-listp new-extdecls).

Definitions and Theorems

Function: simpadd0-extdecl-list

(defun simpadd0-extdecl-list (extdecls)
  (declare (xargs :guard (extdecl-listp extdecls)))
  (declare (xargs :guard (extdecl-list-unambp extdecls)))
  (let ((__function__ 'simpadd0-extdecl-list))
    (declare (ignorable __function__))
    (cond ((endp extdecls) nil)
          (t (cons (simpadd0-extdecl (car extdecls))
                   (simpadd0-extdecl-list (cdr extdecls)))))))

Theorem: extdecl-listp-of-simpadd0-extdecl-list

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

Theorem: extdecl-list-unambp-of-simpadd0-extdecl-list

(defthm extdecl-list-unambp-of-simpadd0-extdecl-list
  (b* ((?new-extdecls (simpadd0-extdecl-list extdecls)))
    (extdecl-list-unambp new-extdecls)))

Theorem: simpadd0-extdecl-list-of-extdecl-list-fix-extdecls

(defthm simpadd0-extdecl-list-of-extdecl-list-fix-extdecls
  (equal (simpadd0-extdecl-list (extdecl-list-fix extdecls))
         (simpadd0-extdecl-list extdecls)))

Theorem: simpadd0-extdecl-list-extdecl-list-equiv-congruence-on-extdecls

(defthm
    simpadd0-extdecl-list-extdecl-list-equiv-congruence-on-extdecls
  (implies (c$::extdecl-list-equiv extdecls extdecls-equiv)
           (equal (simpadd0-extdecl-list extdecls)
                  (simpadd0-extdecl-list extdecls-equiv)))
  :rule-classes :congruence)