		Search-engine friendly clone of the ACL2 documentation.

Preprocessor-states

Update-ppstate->macros

Signature
(update-ppstate->macros macros ppstate) → ppstate
Arguments: macros — Guard (macro-tablep macros).
Returns: ppstate — Type (ppstatep ppstate).

Definitions and Theorems

Function: update-ppstate->macros

(defun update-ppstate->macros (macros ppstate)
  (declare (xargs :stobjs (ppstate)))
  (declare (xargs :guard (macro-tablep macros)))
  (b* ((ppstate (ppstate-fix ppstate)))
    (raw-update-ppstate->macros (macro-table-fix macros)
                                ppstate)))

Theorem: ppstatep-of-update-ppstate->macros

(defthm ppstatep-of-update-ppstate->macros
  (b* ((ppstate (update-ppstate->macros macros ppstate)))
    (ppstatep ppstate))
  :rule-classes :rewrite)

Theorem: update-ppstate->macros-of-macro-table-fix-macros

(defthm update-ppstate->macros-of-macro-table-fix-macros
  (equal (update-ppstate->macros (macro-table-fix macros)
                                 ppstate)
         (update-ppstate->macros macros ppstate)))

Theorem: update-ppstate->macros-macro-table-equiv-congruence-on-macros

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

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

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

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

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