		Search-engine friendly clone of the ACL2 documentation.

Trans-state

Get-trans-state

Get the translation state from the table.

Signature
(get-trans-state wrld) → tstate
Arguments: wrld — Guard (plist-worldp wrld).
Returns: tstate — Type (trans-statep tstate).

Definitions and Theorems

Function: get-trans-state

(defun get-trans-state (wrld)
 (declare (xargs :guard (plist-worldp wrld)))
 (let ((__function__ 'get-trans-state))
  (declare (ignorable __function__))
  (b*
   ((table (table-alist 'trans-state-table wrld)
)
    ((unless (alistp table))
     (raise
      "Internal error: ~
                the translation state table ~x0 is not an alist."
      table)
     (init-trans-state))
    (tstate (cdr (assoc-eq :state table)))
    ((unless (trans-statep tstate))
     (raise
      "Internal error: ~
                the translation state ~x0 is malformed."
      tstate)
     (init-trans-state)))
   tstate)))

Theorem: trans-statep-of-get-trans-state

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