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
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
Make-implicit-wires
Resolve-indexing
Vl-modulelist-resolve-indexing
Vl-expr-resolve-indexing-aux
Vl-exprlist-resolve-indexing-aux
Vl-maybe-delayoreventcontrol-resolve-indexing
Vl-plainarglist-resolve-indexing
Vl-namedarglist-resolve-indexing
Vl-modinstlist-resolve-indexing
Vl-initiallist-resolve-indexing
Vl-gateinstlist-resolve-indexing
Vl-fundecllist-resolve-indexing
Vl-repeateventcontrol-resolve-indexing
Vl-evatomlist-resolve-indexing
Vl-delayoreventcontrol-resolve-indexing
Vl-assignlist-resolve-indexing
Vl-alwayslist-resolve-indexing
Vl-portlist-resolve-indexing
Vl-exprlist-resolve-indexing
Vl-eventcontrol-resolve-indexing
Vl-delaycontrol-resolve-indexing
Vl-arguments-resolve-indexing
Vl-maybe-expr-resolve-indexing
Vl-plainarg-resolve-indexing
Vl-namedarg-resolve-indexing
Vl-gateinst-resolve-indexing
Vl-fundecl-resolve-indexing
Vl-assign-resolve-indexing
Vl-port-resolve-indexing
Vl-modinst-resolve-indexing
Vl-initial-resolve-indexing
Vl-evatom-resolve-indexing
Vl-always-resolve-indexing
Vl-expr-resolve-indexing
Vl-expr-is-bitselect-type
Vl-module-resolve-indexing
Vl-datatype-bitselect-p
Vl-design-resolve-indexing
Origexprs
Argresolve
Portdecl-sign
Designwires
Udp-elim
Vl-annotate-design
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
Vl-expr-resolve-indexing-aux
Vl-exprlist-resolve-indexing-aux
Signature
(vl-exprlist-resolve-indexing-aux x ss warnings) → (mv new-warnings changedp new-x)
Arguments
x
—
Guard
(
vl-exprlist-p
x)
.
ss
—
Guard
(
vl-scopestack-p
ss)
.
warnings
—
Guard
(
vl-warninglist-p
warnings)
.
Returns
new-warnings
—
Type
(
vl-warninglist-p
new-warnings)
.
changedp
—
Type
(
booleanp
changedp)
.
new-x
—
Type
(
and
(
vl-exprlist-p
new-x) (
equal
(
len
new-x) (
len
x)))
.