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
Expression-sizing
Expression-sizing-minutia
Expression-sizing-intro
Vl-keyvalue-pattern-collect-array-replacements
Vl-assignpattern-positional-replacement
Vl-plainarg-exprsize
Vl-assignpattern-keyvalue-replacement
Vl-keyvalue-pattern-collect-struct-replacements
Vl-modulelist-exprsize
Vl-expr-assignpattern-extend/truncate
Vl-structmemberlist->types
Vl-expr-size
Vl-expr-selfdetermine-type
Vl-assignpattern-multi-replacement
Vl-parse-keyval-pattern-struct
Vl-plainarglist-exprsize
Vl-parse-keyval-pattern-array
Vl-warn-about-implicit-extension
Vl-assigncontext-size
Vl-arguments-exprsize
Vl-assignpattern-replacement
Vl-packeddimensionlist-exprsize
Vl-namedparamvaluelist-exprsize
Vl-maybe-delayoreventcontrol-exprsize
Vl-repeateventcontrol-exprsize
Vl-paramvaluelist-exprsize
Vl-maybe-packeddimension-exprsize
Vl-delayoreventcontrol-exprsize
Vl-namedparamvalue-exprsize
Vl-namedarglist-exprsize
Vl-enumitemlist-exprsize
Vl-packeddimension-exprsize
Vl-maybe-paramvalue-exprsize
Vl-evatomlist-exprsize
Vl-atom-selfdetermine-type
Vl-rangelist-exprsize
Vl-maybe-gatedelay-exprsize
Vl-maybe-datatype-exprsize
Vl-gatedelay-exprsize
Vl-paramargs-exprsize
Vl-namedarg-exprsize
Vl-eventcontrol-exprsize
Vl-enumbasetype-exprsize
Vl-delaycontrol-exprsize
Vl-paramvalue-exprsize
Vl-maybe-range-exprsize
Vl-enumitem-exprsize
Vl-range-exprsize
Vl-paramdecl-exprsize
Vl-paramdecllist-exprsize
Vl-maybe-expr-size
Vl-evatom-exprsize
Vl-vardecllist-exprsize
Vl-portdecllist-exprsize
Vl-modinstlist-exprsize
Vl-initiallist-exprsize
Vl-gateinstlist-exprsize
Vl-fundecllist-exprsize
Vl-assign-exprsize
Vl-interfaceport-exprsize
Vl-assignlist-exprsize
Vl-alwayslist-exprsize
Vl-portlist-exprsize
Vl-modinst-exprsize
Vl-gateinst-exprsize
Vl-fundecl-exprsize
Vl-vardecl-exprsize
Vl-regularport-exprsize
Vl-portdecl-exprsize
Vl-initial-exprsize
Vl-always-exprsize
Vl-port-exprsize
Vl-lvalue-type
Vl-classify-extension-warning-hook
Welltyped
Vl-castexpr->datatype
Vl-expr-size-assigncontext
Vl-type-expr-pairs-sum-datatype-sizes
Vl-basictype->datatype
Vl-expr-replace-assignpatterns
Vl-design-exprsize
Vl-op-simple-vector-p
Vl-expr-val-alist-max-count
Vl-expr-has-patterns
Vl-exprlist-max-count
Vl-unsigned-when-size-zero-lst
Vl-type-expr-pairs
Append-n
Vl-expr-val-alist
Vl-datatypelist
Vl-datatypelist-fix
Vl-datatypelist-equiv
Vl-datatypelist-p
Occform
Oprewrite
Expand-functions
Delayredux
Unparameterization
Caseelim
Split
Selresolve
Weirdint-elim
Vl-delta
Replicate-insts
Rangeresolve
Propagate
Clean-selects
Clean-params
Blankargs
Inline-mods
Expr-simp
Trunc
Always-top
Gatesplit
Gate-elim
Expression-optimization
Elim-supplies
Wildelim
Drop-blankports
Clean-warnings
Addinstnames
Custom-transform-hooks
Annotate
Latchcode
Elim-unused-vars
Problem-modules
Lint
Mlib
Server
Kit
Printer
Esim-vl
Well-formedness
Sv
Vwsim
Fgl
Vl
X86isa
Svl
Rtl
Software-verification
Math
Testing-utilities
Expression-sizing
Vl-datatypelist
A list of
vl-datatype-p
objects.
This is an ordinary
fty::deflist
.
Subtopics
Vl-datatypelist-fix
(vl-datatypelist-fix x)
is a usual
ACL2::fty
list fixing function.
Vl-datatypelist-equiv
Basic equivalence relation for
vl-datatypelist
structures.
Vl-datatypelist-p
(vl-datatypelist-p x)
recognizes lists where every element satisfies
vl-datatype-p
.