		Search-engine friendly clone of the ACL2 documentation.

Printer

Print-ext-declon

Print an external declaration.

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

Definitions and Theorems

Function: print-ext-declon

(defun print-ext-declon (extdecl pstate)
 (declare (xargs :guard (and (ext-declonp extdecl)
                             (pristatep pstate))))
 (declare
  (xargs :guard
         (and (ext-declon-unambp extdecl)
              (ext-declon-aidentp extdecl (pristate->gcc pstate)))))
 (let ((__function__ 'print-ext-declon))
   (declare (ignorable __function__))
   (ext-declon-case extdecl :fundef
                    (print-fundef extdecl.fundef pstate)
                    :declon
                    (print-declon extdecl.declon pstate)
                    :empty
                    (b* ((pstate (print-astring ";" pstate))
                         (pstate (print-new-line pstate)))
                      pstate)
                    :asm (print-asm-stmt extdecl.stmt pstate))))

Theorem: pristatep-of-print-ext-declon

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

Theorem: pristate->gcc-of-print-ext-declon

(defthm pristate->gcc-of-print-ext-declon
  (b* ((?new-pstate (print-ext-declon extdecl pstate)))
    (equal (pristate->gcc new-pstate)
           (pristate->gcc pstate))))

Theorem: print-ext-declon-of-ext-declon-fix-extdecl

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

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

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

Theorem: print-ext-declon-of-pristate-fix-pstate

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

Theorem: print-ext-declon-pristate-equiv-congruence-on-pstate

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