		Search-engine friendly clone of the ACL2 documentation.

Trans-state

Extend-trans-state

Extend the translation state with a Syntheto top-level construct.

Signature
(extend-trans-state top tstate) → new-tstate
Arguments: top — Guard (toplevelp top).; tstate — Guard (trans-statep tstate).
Returns: new-tstate — Type (trans-statep new-tstate).

This is consed to the list, which is in reverse chronological order.

Definitions and Theorems

Function: extend-trans-state

(defun extend-trans-state (top tstate)
 (declare (xargs :guard (and (toplevelp top)
                             (trans-statep tstate))))
 (let ((__function__ 'extend-trans-state))
  (declare (ignorable __function__))
  (change-trans-state tstate
                      :tops (cons top (trans-state->tops tstate)))))

Theorem: trans-statep-of-extend-trans-state

(defthm trans-statep-of-extend-trans-state
  (b* ((new-tstate (extend-trans-state top tstate)))
    (trans-statep new-tstate))
  :rule-classes :rewrite)

Theorem: extend-trans-state-of-toplevel-fix-top

(defthm extend-trans-state-of-toplevel-fix-top
  (equal (extend-trans-state (toplevel-fix top)
                             tstate)
         (extend-trans-state top tstate)))

Theorem: extend-trans-state-toplevel-equiv-congruence-on-top

(defthm extend-trans-state-toplevel-equiv-congruence-on-top
  (implies (toplevel-equiv top top-equiv)
           (equal (extend-trans-state top tstate)
                  (extend-trans-state top-equiv tstate)))
  :rule-classes :congruence)

Theorem: extend-trans-state-of-trans-state-fix-tstate

(defthm extend-trans-state-of-trans-state-fix-tstate
  (equal (extend-trans-state top (trans-state-fix tstate))
         (extend-trans-state top tstate)))

Theorem: extend-trans-state-trans-state-equiv-congruence-on-tstate

(defthm extend-trans-state-trans-state-equiv-congruence-on-tstate
  (implies (trans-state-equiv tstate tstate-equiv)
           (equal (extend-trans-state top tstate)
                  (extend-trans-state top tstate-equiv)))
  :rule-classes :congruence)