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
Svex-stvs
Svex-decomposition-methodology
Sv-versus-esim
Svex-decomp
Svex-compose-dfs
Svex-compilation
Moddb
Svmods
Svstmt
Sv-tutorial
Expressions
Rewriting
Svex
Bit-blasting
Functions
4vmask
Why-infinite-width
Svex-vars
Evaluation
Svex-xeval
4vec-xfree-p
Svexlist-xeval
Svex-fn/args-xeval
Svex-call-xeval
Svex-mono-eval
Svex-eval
Svex-apply
Svex-env
Svex-alist-eval
Svar-boolmasks-lookup
Svex-s4eval
Svexlist-unquote
Svex-alist-eval-for-symbolic
Svexlist-eval
Svexlist-quotesp
Svar-boolmasks
Svexlist-s4eval
Svexlist-eval-for-symbolic
Values
Symbolic-test-vector
Vl-to-svex
Vwsim
Fgl
Vl
X86isa
Svl
Rtl
Software-verification
Math
Testing-utilities
Svex-xeval
Svexlist-xeval
Maps
svex-xeval
over an
svex
list.
Signature
(svexlist-xeval x) → val
Arguments
x
—
Guard
(
svexlist-p
x)
.
Returns
val
—
Type
(
4veclist-p
val)
.