• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
        • Error-checking
        • Fty-extensions
        • Isar
        • Kestrel-utilities
          • Omaps
          • Directed-untranslate
          • Include-book-paths
          • Ubi
          • Numbered-names
          • Digits-any-base
          • Context-message-pair
          • With-auto-termination
          • Make-termination-theorem
          • Theorems-about-true-list-lists
          • Checkpoint-list
          • Sublis-expr+
          • Integers-from-to
          • Prove$
          • Defthm<w
          • System-utilities-non-built-in
            • Pseudo-event-formp
            • Pseudo-event-form-listp
            • Directed-untranslate
            • Irrelevant-formals-info
            • Numbered-names
            • Context-message-pair
            • Prove$
            • Minimize-ruler-extenders
            • Paired-names
            • Orelse
            • Fresh-name-in-world-with-$s
            • Encapsulate-report-errors
            • On-failure
            • Chk-irrelevant-formals-ok
            • Named-formulas
            • Pseudo-event-landmarkp
            • All-program-fns
            • All-logic-fns
            • Trans-eval-error-triple
            • Trans-eval-state
              • Pseudo-tests-and-callsp
              • User-interface
              • Pseudo-command-landmarkp
              • Pseudo-tests-and-calls-listp
              • Pseudo-command-formp
              • Orelse*
              • Identity-macro
            • Integer-range-fix
            • Minimize-ruler-extenders
            • Add-const-to-untranslate-preprocess
            • Unsigned-byte-fix
            • Signed-byte-fix
            • Defthmr
            • Paired-names
            • Unsigned-byte-list-fix
            • Signed-byte-list-fix
            • Show-books
            • Skip-in-book
            • Typed-tuplep
            • List-utilities
            • Checkpoint-list-pretty
            • Defunt
            • Keyword-value-list-to-alist
            • Magic-macroexpand
            • Top-command-number-fn
            • Bits-as-digits-in-base-2
            • Show-checkpoint-list
            • Ubyte11s-as-digits-in-base-2048
            • Named-formulas
            • Bytes-as-digits-in-base-256
            • String-utilities
            • Make-keyword-value-list-from-keys-and-value
            • Defmacroq
            • Integer-range-listp
            • Apply-fn-if-known
            • Trans-eval-error-triple
            • Checkpoint-info-list
            • Previous-subsumer-hints
            • Fms!-lst
            • Zp-listp
            • Trans-eval-state
              • Injections
              • Doublets-to-alist
              • Theorems-about-osets
              • Typed-list-utilities
              • Book-runes-alist
              • User-interface
              • Bits/ubyte11s-digit-grouping
              • Bits/bytes-digit-grouping
              • Message-utilities
              • Subsetp-eq-linear
              • Oset-utilities
              • Strict-merge-sort-<
              • Miscellaneous-enumerations
              • Maybe-unquote
              • Thm<w
              • Defthmd<w
              • Io-utilities
            • Set
            • Soft
            • C
            • Bv
            • Imp-language
            • Event-macros
            • Java
            • Bitcoin
            • Ethereum
            • Yul
            • Zcash
            • ACL2-programming-language
            • Prime-fields
            • Json
            • Syntheto
            • File-io-light
            • Cryptography
            • Number-theory
            • Lists-light
            • Axe
            • Builtins
            • Solidity
            • Helpers
            • Htclient
            • Typed-lists-light
            • Arithmetic-light
          • X86isa
          • Axe
          • Execloader
        • Math
        • Testing-utilities
      • Kestrel-utilities
      • System-utilities-non-built-in

      Trans-eval-state

      An ACL2 evaluator that returns state

      General Form:
      
      (trans-eval-state form ctx state)

      where form is a form to evaluate, ctx is a context (see ctx), and state is the ACL2 state. After form is (translated to internal form and) evaluated, the new ACL2 state is returned. See trans-eval-error-triple for a potentially more useful version of this function that returns an error-triple, which provides an error and value as well rather than just a new state.