		Search-engine friendly clone of the ACL2 documentation.

Trans-state

Init-trans-state

Initial translation state.

Signature
(init-trans-state) → tstate
Returns: tstate — Type (trans-statep tstate).

Definitions and Theorems

Function: init-trans-state

(defun init-trans-state nil
  (declare (xargs :guard t))
  (let ((__function__ 'init-trans-state))
    (declare (ignorable __function__))
    (make-trans-state :tops nil)))

Theorem: trans-statep-of-init-trans-state

(defthm trans-statep-of-init-trans-state
  (b* ((tstate (init-trans-state)))
    (trans-statep tstate))
  :rule-classes :rewrite)