		Search-engine friendly clone of the ACL2 documentation.

Preprocessor-states

Ppstate->macros

Signature
(ppstate->macros ppstate) → macros
Returns: macros — Type (macro-tablep macros).

Definitions and Theorems

Function: ppstate->macros

(defun ppstate->macros (ppstate)
  (declare (xargs :stobjs (ppstate)))
  (declare (xargs :guard t))
  (mbe :logic
       (if (ppstatep ppstate)
           (raw-ppstate->macros ppstate)
         (macro-table-init))
       :exec (raw-ppstate->macros ppstate)))

Theorem: macro-tablep-of-ppstate->macros

(defthm macro-tablep-of-ppstate->macros
  (b* ((macros (ppstate->macros ppstate)))
    (macro-tablep macros))
  :rule-classes :rewrite)

Theorem: ppstate->macros-of-ppstate-fix-ppstate

(defthm ppstate->macros-of-ppstate-fix-ppstate
  (equal (ppstate->macros (ppstate-fix ppstate))
         (ppstate->macros ppstate)))

Theorem: ppstate->macros-ppstate-equiv-congruence-on-ppstate

(defthm ppstate->macros-ppstate-equiv-congruence-on-ppstate
  (implies (ppstate-equiv ppstate ppstate-equiv)
           (equal (ppstate->macros ppstate)
                  (ppstate->macros ppstate-equiv)))
  :rule-classes :congruence)