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
Symbolic-test-vector
Vl-to-svex
Vl-to-sv
Vl-design->sv-design
Vl-simpconfig
Vl-hierarchy-sv-translation
Vl-expr-svex-translation
Sv::vl-expr.lisp
Vttree
Vttree-p
Vttree-fix
Vttree-count
Vttree-equiv
Vttree-context
Vttree-branch
Vttree-branch->right
Make-vttree-branch
Vttree-branch->left
Change-vttree-branch
Vttree-warnings
Vttree-constraints
Vttree-none
Vttree-kind
Patbind-wvmv
Patbind-vwmv
Patbind-vmv
Vl-design->svex-modalist
Vl-svstmt
Vl-to-sv-main
Vl-simplify-sv
Vl-user-paramsettings->unparam-names
Vl-user-paramsettings->modnames
Vwsim
Fgl
Vl
X86isa
Svl
Rtl
Software-verification
Math
Testing-utilities
Vttree
Vttree-branch
This is a product type, introduced by
defflexsum
in support of
vttree
.
Fields
left —
vttree
right —
vttree
Subtopics
Vttree-branch->right
Get the
right
field from a
vttree-branch
.
Make-vttree-branch
Basic constructor macro for
vttree-branch
structures.
Vttree-branch->left
Get the
left
field from a
vttree-branch
.
Change-vttree-branch
Modifying constructor for
vttree-branch
structures.