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-assign
Svstmt-compile
Svstmt-compile.lisp
Svstate-merge-branches
Svex-alist-merge-branches
Svstmt-assign->subst
Svstack-merge-branches
Svstacks-compatible
Svjumpstate-merge-svstate-branches
Svjumpstate-svstate-compatible
Svstmt-lhs-check-masks
Svjumpstate
Svjumpstates-compatible
Svstmtlist-compile-top
Svjumpstate-sequence-svstates
Constraintlist-merge-branches
Svjumpstate-merge-branches
Svex-replace-range
Svex-svstmt-ite
Svstmt-process-write
Svjumpstate-sequence
Svstmt-process-writelist
Svstack-assign
Svstmt-writelist-var-sizes
Svstates-compatible
4vec-replace-range
Svstmt-write-var-sizes
Make-empty-svjumpstate
Constraintlist-add-pathcond
Svjumpstate-pop-scope
Constraintlist-compose-svstack
Svstack-to-svex-alist
Svstack-filter-global-lhs-vars
Svjumpstate-vars
Svex-svstmt-or
Svex-svstmt-andc1
Svstate-push-scope
Svstate-pop-scope
Svstate-vars
Svstack-lookup
Svar-subtract-delay
Svstmt-initialize-locals
Svstack-fork
Svstack-clean
Svstack-nonempty-fix
Svstate-fork
Svstate-clean
Svstack-globalp
Svjumpstate-fork
Svar-delayed-member
Svjumpstate-levels
Svjumpstate-free
Svstate-free
Svstack-free
Svstack
Svar-size-alist
Svar-size-alist-p
Svar-size-alist-fix
Svar-size-alist-equiv
Svstate
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-compile.lisp
Svar-size-alist
An alist mapping
svar-p
to
natp
.
This is an ordinary
defalist
.
Subtopics
Svar-size-alist-p
Recognizer for
svar-size-alist
.
Svar-size-alist-fix
(svar-size-alist-fix x)
is an
fty
alist fixing function that follows the fix-keys strategy.
Svar-size-alist-equiv
Basic equivalence relation for
svar-size-alist
structures.