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
Warnings
Primitives
Use-set
Syntax
Getting-started
Utilities
Loader
Transforms
Lint
Mlib
Scopestack
Filtering-by-name
Vl-namefactory
Substitution
Allexprs
Vl-packeddimensionlist-allexprs
Vl-namedparamvaluelist-allexprs
Vl-paramvaluelist-allexprs
Vl-paramdecllist-allexprs
Vl-vardecllist-allexprs
Vl-taskdecllist-allexprs
Vl-portdecllist-allexprs
Vl-plainarglist-allexprs
Vl-namedarglist-allexprs
Vl-modinstlist-allexprs
Vl-initiallist-allexprs
Vl-gateinstlist-allexprs
Vl-fundecllist-allexprs
Vl-enumitemlist-allexprs
Vl-rangelist-allexprs
Vl-modulelist-allexprs
Vl-evatomlist-allexprs
Vl-assignlist-allexprs
Vl-alwayslist-allexprs
Vl-aliaslist-allexprs
Vl-portlist-allexprs
Vl-maybe-delayoreventcontrol-allexprs
Vl-maybe-packeddimension-allexprs
Vl-delayoreventcontrol-allexprs
Vl-repeateventcontrol-allexprs
Vl-packeddimension-allexprs
Vl-namedparamvalue-allexprs
Vl-module-allexprs
Vl-maybe-paramvalue-allexprs
Vl-maybe-gatedelay-allexprs
Vl-paramtype-allexprs
Vl-maybe-datatype-allexprs
Vl-taskdecl-allexprs
Vl-paramvalue-allexprs
Vl-paramargs-allexprs
Vl-modinst-allexprs
Vl-maybe-range-allexprs
Vl-maybe-expr-allexprs
Vl-gateinst-allexprs
Vl-gatedelay-allexprs
Vl-fundecl-allexprs
Vl-eventcontrol-allexprs
Vl-enumitem-allexprs
Vl-enumbasetype-allexprs
Vl-delaycontrol-allexprs
Vl-arguments-allexprs
Vl-vardecl-allexprs
Vl-portdecl-allexprs
Vl-plainarg-allexprs
Vl-paramdecl-allexprs
Vl-namedarg-allexprs
Vl-datatype-allexprs
Vl-datatype-allexprs-nrev
Vl-structmemberlist-allexprs
Vl-structmember-allexprs
Vl-assign-allexprs
Vl-range-allexprs
Vl-port-allexprs
Vl-initial-allexprs
Vl-evatom-allexprs
Vl-always-allexprs
Vl-alias-allexprs
Vl-stmt-allexprs
Hid-tools
Vl-consteval
Range-tools
Lvalexprs
Hierarchy
Finding-by-name
Expr-tools
Expr-slicing
Stripping-functions
Stmt-tools
Modnamespace
Vl-parse-expr-from-str
Welltyped
Reordering-by-name
Flat-warnings
Genblob
Expr-building
Datatype-tools
Syscalls
Relocate
Expr-cleaning
Namemangle
Caremask
Port-tools
Lvalues
Server
Kit
Printer
Esim-vl
Well-formedness
Sv
Vwsim
Fgl
Vl
X86isa
Svl
Rtl
Software-verification
Math
Testing-utilities
Vl-datatype-allexprs
Vl-structmember-allexprs
Signature
(vl-structmember-allexprs x) → exprs
Arguments
x
—
Guard
(
vl-structmember-p
x)
.
Returns
exprs
—
Type
(
vl-exprlist-p
exprs)
.