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
Values
4vec
4vec-operations
4vec-p
S4vecs
4vec-examples
Maybe-4vec
4vec-equiv
Make-4vec
4vec->upper
4vec->lower
4veclist
4veclist-fix
4veclist-p
4veclist-<<=
4veclist-nth-safe
4veclist-equiv
4vec-fix
Make-honsed-4vec
4vec-index-p
4vec-<<=
3vec
2vec
2vecx
2vecnatx
4vec-x
4vec-1x
4vec-1z
4vec-z
Symbolic-test-vector
Vl-to-svex
Vwsim
Fgl
Vl
X86isa
Svl
Rtl
Software-verification
Math
Testing-utilities
4vec
4veclist
A list of
4vec-p
objects.
This is an ordinary
deflist
.
Subtopics
4veclist-fix
(4veclist-fix x)
is a usual
fty
list fixing function.
4veclist-p
(4veclist-p x)
recognizes lists where every element satisfies
4vec-p
.
4veclist-<<=
Nth-wise lattice ordering for
4veclist
s.
4veclist-nth-safe
Like
nth
but, with proper
fty-discipline
for
4veclist
s. ``Safely'' causes a run-time error if
n
is out of bounds.
4veclist-equiv
Basic equivalence relation for
4veclist
structures.