		Search-engine friendly clone of the ACL2 documentation.

Printer

Print-extdecl

Print an external declaration.

Signature
(print-extdecl extdecl pstate) → new-pstate
Arguments: extdecl — Guard (extdeclp extdecl).; pstate — Guard (pristatep pstate).
Returns: new-pstate — Type (pristatep new-pstate).

Definitions and Theorems

Function: print-extdecl

(defun print-extdecl (extdecl pstate)
  (declare (xargs :guard (and (extdeclp extdecl)
                              (pristatep pstate))))
  (declare (xargs :guard (extdecl-unambp extdecl)))
  (let ((__function__ 'print-extdecl))
    (declare (ignorable __function__))
    (extdecl-case extdecl :fundef
                  (print-fundef extdecl.unwrap pstate)
                  :decl (print-decl extdecl.unwrap pstate)
                  :empty
                  (b* ((pstate (print-astring ";" pstate))
                       (pstate (print-new-line pstate)))
                    pstate)
                  :asm (print-asm-stmt extdecl.unwrap pstate))))

Theorem: pristatep-of-print-extdecl

(defthm pristatep-of-print-extdecl
  (b* ((new-pstate (print-extdecl extdecl pstate)))
    (pristatep new-pstate))
  :rule-classes :rewrite)

Theorem: print-extdecl-of-extdecl-fix-extdecl

(defthm print-extdecl-of-extdecl-fix-extdecl
  (equal (print-extdecl (extdecl-fix extdecl)
                        pstate)
         (print-extdecl extdecl pstate)))

Theorem: print-extdecl-extdecl-equiv-congruence-on-extdecl

(defthm print-extdecl-extdecl-equiv-congruence-on-extdecl
  (implies (extdecl-equiv extdecl extdecl-equiv)
           (equal (print-extdecl extdecl pstate)
                  (print-extdecl extdecl-equiv pstate)))
  :rule-classes :congruence)

Theorem: print-extdecl-of-pristate-fix-pstate

(defthm print-extdecl-of-pristate-fix-pstate
  (equal (print-extdecl extdecl (pristate-fix pstate))
         (print-extdecl extdecl pstate)))

Theorem: print-extdecl-pristate-equiv-congruence-on-pstate

(defthm print-extdecl-pristate-equiv-congruence-on-pstate
  (implies (pristate-equiv pstate pstate-equiv)
           (equal (print-extdecl extdecl pstate)
                  (print-extdecl extdecl pstate-equiv)))
  :rule-classes :congruence)