Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Projects
Debugging
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
Math
Testing-utilities
Vl-translation-p
Vl-translation->filemap
Access the
filemap
field of a
vl-translation-p
structure.