Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Debugging
Projects
Std
Proof-automation
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
Gl
Esim
Vl2014
Sv
Vwsim
Fgl
Vl
Syntax
Loader
Warnings
Getting-started
Utilities
Printer
Kit
Mlib
Scopestack
Hid-tools
Filtering-by-name
Vl-interface-mocktype
Stripping-functions
Genblob
Expr-tools
Extract-vl-types
Hierarchy
Range-tools
Finding-by-name
Stmt-tools
Vl-rebuild-caselist
Vl-stmt-atomicstmts
Vl-compoundstmt->stmts
Vl-compoundstmt->exprs
Vl-compoundstmt->vardecls
Change-vl-compoundstmt
Vl-compoundstmt->paramdecls
Vl-compoundstmt->ctrl
Vl-atomicstmtlist-p
Vl-stmt->atts
Vl-atomicstmt-p
Vl-timingstmt-p
Vl-repeatstmt-p
Vl-foreverstmt-p
Vl-assignstmt-p
Vl-whilestmt-p
Vl-waitstmt-p
Vl-nullstmt-p
Vl-ifstmt-p
Vl-forstmt-p
Vl-dostmt-p
Vl-casestmt-p
Vl-callstmt-p
Vl-exprlistlist
Vl-exprlistlist-fix
Vl-exprlistlist-equiv
Vl-exprlistlist-p
Modnamespace
Flat-warnings
Reordering-by-name
Datatype-tools
Syscalls
Allexprs
Lvalues
Port-tools
Transforms
X86isa
Svl
Rtl
Software-verification
Math
Testing-utilities
Stmt-tools
Vl-exprlistlist
A list of
vl-exprlist-p
objects.
This is an ordinary
fty::deflist
.
Subtopics
Vl-exprlistlist-fix
(vl-exprlistlist-fix x)
is a usual
fty
list fixing function.
Vl-exprlistlist-equiv
Basic equivalence relation for
vl-exprlistlist
structures.
Vl-exprlistlist-p
(vl-exprlistlist-p x)
recognizes lists where every element satisfies
vl-exprlist-p
.