• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
      • Symbolic-test-vectors
      • Esim-primitives
      • E-conversion
      • Esim-steps
      • Patterns
      • Mod-internal-paths
      • Defmodules
        • Vl-translation-p
          • Vl-translation
          • Make-vl-translation
          • Change-vl-translation
          • Vl-translation-has-module
          • Honsed-vl-translation
          • Make-honsed-vl-translation
          • Vl-translation-get-esim
          • Vl-translation->orig
          • Vl-translation->good
          • Vl-translation->filemap
          • Vl-translation->defines
          • Vl-translation->bad
        • Vl-simplify
        • Defmodules-fn
      • Esim-simplify-update-fns
      • Esim-tutorial
      • Esim-vl
    • Vl2014
    • Sv
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Testing-utilities
  • Math

• Vl-translation-p

Vl-translation->orig

Access the orig field of a vl-translation-p structure.