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
Svtv-data
Defsvtv$
Svtv-run
Defsvtv-phasewise
Svtv-spec
Svtv
Defsvtv
Process.lisp
Svtv-doc
Svtv-chase$
Svtv-versus-stv
Svtv-debug-fsm
Structure.lisp
Svtv-baseentry-p
Svtv-entry-p
Svtv-outentry-p
Svtv-outentry-fix
Svtv-baseentry-fix
Svtv-entry-fix
Svtv-overrideline
Svtv-outputline
Svtv-condoverride
Svtv-line
Svtv-inputmap
Svtv-outentrylist
Svtv-lines
Svtv-lines-fix
Svtv-lines-p
Svtv-lines-equiv
Svtv-entrylist
Svtv-overridelines
Svtv-outputs
Svtv-inputtype-p
Svtv-dontcare-p
Svtv-debug
Def-pipeline-thm
Expand.lisp
Def-cycle-thm
Svtv-utilities
Svtv-debug$
Defsvtv$-phasewise
Svex-decomposition-methodology
Sv-versus-esim
Svex-decomp
Svex-compose-dfs
Svex-compilation
Moddb
Svmods
Svstmt
Sv-tutorial
Expressions
Symbolic-test-vector
Vl-to-svex
Vwsim
Fgl
Vl
X86isa
Svl
Rtl
Software-verification
Math
Testing-utilities
Structure.lisp
Svtv-lines
A list of
svtv-line-p
objects.
This is an ordinary
deflist
.
Subtopics
Svtv-lines-fix
(svtv-lines-fix x)
is a usual
fty
list fixing function.
Svtv-lines-p
(svtv-lines-p x)
recognizes lists where every element satisfies
svtv-line-p
.
Svtv-lines-equiv
Basic equivalence relation for
svtv-lines
structures.