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
Warnings
Getting-started
Utilities
Printer
Kit
Mlib
Scopestack
Hid-tools
Filtering-by-name
Vl-interface-mocktype
Stripping-functions
Genblob
Expr-tools
Vl-expr-typedecide
Vl-exprlist-resolved->vals
Vl-make-idexpr-list
Vl-idexprlist->names
Vl-expr-selfsize
Vl-tweak-fussy-warning-type
Vl-interesting-size-atoms
Vl-exprlist-interesting-size-atoms
Vl-expr-interesting-size-atoms
Vl-collect-unsized-ints
Vl-unsized-index-p
Vl-tweak-fussy-warning-type-preclean
Vl-collect-resolved-exprs
Vl-tweak-fussy-warning-type-arithop
Nats-below-p
Vl-binaryop-selfsize
Vl-expr-opacity
Vl-unaryop-selfsize
Vl-exprlist-selfsize
Vl-expr-update-subexprs
Vl-exprlist-to-plainarglist
Vl-call-namedargs-update-subexprs
Vl-valuerangelist-update-subexprs
Vl-streamexprlist-update-subexprs
Vl-op-p
Vl-maybe-exprlist-update-subexprs
Vl-evatomlist-update-subexprs
Vl-expr-values
Vl-keyvallist-update-subexprs
Vl-assignpat-update-subexprs
Vl-valuerange-update-subexprs
Vl-scopeexpr-update-subexprs
Vl-partselect-update-subexprs
Vl-hidexpr-update-subexprs
Vl-expr-add-atts
Vl-arrayrange-update-subexprs
Vl-streamexpr-update-subexprs
Vl-slicesize-update-subexprs
Vl-plusminus-update-subexprs
Vl-patternkey-update-subexprs
Vl-expr-ops
Vl-make-integer
Vl-range-update-subexprs
Vl-idexpr
Vl-make-index
Vl-expr->subexprs
Vl-bitlist-from-nat
Vl-pps-expr
Vl-maybe-exprlist->subexprs
Vl-hidexpr->subexprs
Vl-evatomlist->subexprs
Vl-call-namedargs->subexprs
Vl-valuerangelist->subexprs
Vl-streamexprlist->subexprs
Vl-keyvallist->subexprs
Vl-exprlist-has-ops
Vl-expr-resolved-p
Vl-valuerange->subexprs
Vl-streamexpr->subexprs
Vl-slicesize->subexprs
Vl-scopeexpr->subexprs
Vl-patternkey->subexprs
Vl-partselect->subexprs
Vl-assignpat->subexprs
Vl-arrayrange->subexprs
Vl-pps-origexpr
Vl-plusminus->subexprs
Vl-idscope
Vl-idexpr->name
Vl-expr-has-ops
Vl-resolved->val
Vl-range->subexprs
Vl-idexpr-p
Vl-idexprlist-p
Vl-exprlist-resolved-p
Vl-idscope->name
Vl-idscope-p
Vl-zbitlist-p
Vl-zatom-p
Vl-op-fix
Vl-oplist
Vl-expr-varnames
Vl-one-bit-constants
Extract-vl-types
Hierarchy
Range-tools
Finding-by-name
Stmt-tools
Modnamespace
Flat-warnings
Reordering-by-name
Datatype-tools
Syscalls
Allexprs
Lvalues
Port-tools
Transforms
X86isa
Svl
Rtl
Software-verification
Math
Testing-utilities
Vl-interesting-size-atoms
Vl-exprlist-interesting-size-atoms
Signature
(vl-exprlist-interesting-size-atoms x) → vals
Arguments
x
—
Guard
(
vl-exprlist-p
x)
.
Returns
vals
—
Type
(
vl-exprlist-p
vals)
.