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-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
Vl-descriptionlist-fix
Vl-descriptionlist-p
Vl-descriptionlist-equiv
Warnings
Getting-started
Utilities
Printer
Kit
Mlib
Transforms
X86isa
Svl
Rtl
Software-verification
Math
Testing-utilities
Loader
Vl-descriptionlist
A list of
vl-description-p
objects.
This is an ordinary
fty::deflist
.
Subtopics
Vl-descriptionlist-fix
(vl-descriptionlist-fix x)
is a usual
fty
list fixing function.
Vl-descriptionlist-p
(vl-descriptionlist-p x)
recognizes lists where every element satisfies
vl-description-p
.
Vl-descriptionlist-equiv
Basic equivalence relation for
vl-descriptionlist
structures.