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
Svstmt-case
Svstmt-while
Svstmt-p
Svstmt-if
Svstmt-equiv
Svstmt-xcond
Svstmt-scope
Svstmt-scope->locals
Make-svstmt-scope
Svstmt-scope->body
Change-svstmt-scope
Svstmt-assign
Svstmt-compile
Svstmt-constraints
Svstmt-jump
Svstmtlist
Svstmt-kind
Svstmt.lisp
Svstmt-fix
Svstmt-count
Sv-tutorial
Expressions
Symbolic-test-vector
Vl-to-svex
Vwsim
Fgl
Vl
X86isa
Svl
Rtl
Software-verification
Math
Testing-utilities
Svstmt
Svstmt-scope
This is a product type, introduced by
deftagsum
in support of
svstmt
.
Fields
locals —
svarlist
body —
svstmtlist
Subtopics
Svstmt-scope->locals
Get the
locals
field from a
svstmt-scope
.
Make-svstmt-scope
Basic constructor macro for
svstmt-scope
structures.
Svstmt-scope->body
Get the
body
field from a
svstmt-scope
.
Change-svstmt-scope
Modifying constructor for
svstmt-scope
structures.