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
Hid-tools
Vl-consteval
Range-tools
Lvalexprs
Hierarchy
Finding-by-name
Expr-tools
Vl-expr-widthsfixed-p
Vl-exprlist-widthsfixed-p
Vl-make-idexpr-list
Vl-exprlist-resolved->vals
Vl-idexprlist->names
Vl-expr-names
Vl-expr-count
Vl-idexpr
Vl-exprlist-to-plainarglist
Vl-expr-atoms
Vl-expr-ops
Vl-expr-count-noatts
Vl-make-index
Vl-expr-selects
Vl-bitlist-from-nat
Vl-pps-expr
Vl-expr-add-atts
Vl-idexprlist-p
Vl-expr-resolved-p
Vl-pps-origexpr
Vl-expr-funnames
Vl-idexpr->name
Vl-idexpr-p
Vl-exprlist-funnames
Vl-resolved->val
Vl-exprlist-resolved-p
Vl-expr->atts
Vl-obviously-true-expr-p
Vl-obviously-false-expr-p
Vl-exprlist-has-funcalls
Vl-expr-has-funcalls
Vl-zbitlist-p
Vl-zatom-p
Vl-exprlist-has-ops
Vl-expr-has-ops
Vl-expr-varnames
Vl-one-bit-constants
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-expr-widthsfixed-p
Vl-exprlist-widthsfixed-p
Signature
(vl-exprlist-widthsfixed-p x) → *
Arguments
x
—
Guard
(
vl-exprlist-p
x)
.