		Search-engine friendly clone of the ACL2 documentation.

Simpadd0

Simpadd0-extdecl

Transform an external declaration.

Signature
(simpadd0-extdecl extdecl) → new-extdecl
Arguments: extdecl — Guard (extdeclp extdecl).
Returns: new-extdecl — Type (extdeclp new-extdecl).

Definitions and Theorems

Function: simpadd0-extdecl

(defun simpadd0-extdecl (extdecl)
  (declare (xargs :guard (extdeclp extdecl)))
  (declare (xargs :guard (extdecl-unambp extdecl)))
  (let ((__function__ 'simpadd0-extdecl))
    (declare (ignorable __function__))
    (extdecl-case
         extdecl
         :fundef (extdecl-fundef (simpadd0-fundef extdecl.unwrap))
         :decl (extdecl-decl (simpadd0-decl extdecl.unwrap))
         :empty (extdecl-empty)
         :asm (extdecl-fix extdecl))))

Theorem: extdeclp-of-simpadd0-extdecl

(defthm extdeclp-of-simpadd0-extdecl
  (b* ((new-extdecl (simpadd0-extdecl extdecl)))
    (extdeclp new-extdecl))
  :rule-classes :rewrite)

Theorem: extdecl-unambp-of-simpadd0-extdecl

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

Theorem: simpadd0-extdecl-of-extdecl-fix-extdecl

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

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

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