		Search-engine friendly clone of the ACL2 documentation.

Svstmt-compile.lisp

Svstate-merge-branches
Svex-alist-merge-branches
Svstmt-assign->subst
Svstack-merge-branches
Svstacks-compatible: Predicate that describes two svstacks that are in the same scope, but may have different values for the bound variables.
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: A list of svex-alist-p objects.
Svar-size-alist: An alist mapping svar-p to natp.