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
Vl2014
Sv
Vwsim
Fgl
Vl
Syntax
Loader
Preprocessor
Vl-loadconfig
Vl-loadstate
Lexer
Parser
Vl-load-merge-descriptions
Vl-find-basename/extension
Vl-load-file
Vl-loadresult
Scope-of-defines
Vl-find-file
Vl-flush-out-descriptions
Vl-description
Vl-read-file
Vl-includeskips-report-gather
Vl-load-main
Extended-characters
Vl-location
Vl-location-p
Vl-string-between-locs
Vl-location-between-p
Vl-string-findloc
Vl-linecol
Vl-location-string
Vl-location-fix
Vl-location->line
Vl-location->filename
Vl-location->col
Vl-locationlist
Vl-locationlist-fix
Vl-locationlist-equiv
Vl-locationlist-p
*vl-fakeloc*
Vl-echar-p
Vl-echarlist->chars
Vl-echarlist-from-chars
Vl-echarlist-from-str
Vl-echarlist-unsigned-value
Vl-change-echarlist-locations
Vl-echar-digit-value
Vl-echarlist->string
Vl-load
Vl-load-description
Vl-descriptions-left-to-load
Inject-warnings
Vl-preprocess-debug
Vl-write-preprocessor-debug-file
Vl-read-file-report-gather
Vl-load-descriptions
Vl-load-files
Translate-off
Vl-load-read-file-hook
Vl-read-file-report
Vl-loadstate-pad
Vl-load-summary
Vl-collect-modules-from-descriptions
Vl-loadstate->warnings
Vl-iskips-report
Vl-descriptionlist
Warnings
Getting-started
Utilities
Printer
Kit
Mlib
Transforms
X86isa
Svl
Rtl
Software-verification
Math
Testing-utilities
Vl-location
Vl-locationlist
A list of
vl-location-p
objects.
This is an ordinary
fty::deflist
.
Subtopics
Vl-locationlist-fix
(vl-locationlist-fix x)
is a usual
fty
list fixing function.
Vl-locationlist-equiv
Basic equivalence relation for
vl-locationlist
structures.
Vl-locationlist-p
(vl-locationlist-p x)
recognizes lists where every element satisfies
vl-location-p
.