Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Projects
Debugging
Community
Std
Proof-automation
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
Software-verification
Kestrel-books
Crypto-hdwallet
Apt
Error-checking
Fty-extensions
Isar
Kestrel-utilities
Set
C
Syntax-for-tools
Atc
Transformation-tools
Simpadd0
Proof-generation
Split-gso
Wrap-fn
Constant-propagation
Specialize
Split-fn
Split-fn-when
Split-all-gso
Copy-fn
Variables-in-computation-states
Rename
Utilities
Free-vars
Abstract-syntax-rename-fn
Call-graphs
Fresh-ident-utility
Collect-idents
Abstract-syntax-collect-idents
Exprs/decls/stmts-collect-idents
Filepath-transunit-map-collect-idents
Transunit-ensemble-collect-idents
Ext-declon-list-collect-idents
Fundef-option-collect-idents
Ext-declon-collect-idents
Ident-option-collect-idents
Ident-list-collect-idents
Transunit-collect-idents
Fundef-collect-idents
Ident-collect-idents
Typequal/attribspec-list-list-collect-idents
Typequal/attribspec-list-collect-idents
Typequal/attribspec-collect-idents
Struct-declor-list-collect-idents
Struct-declon-list-collect-idents
Param-declon-list-collect-idents
Dirabsdeclor-option-collect-idents
Const-expr-option-collect-idents
Amb-declor/absdeclor-collect-idents
Type-spec-collect-idents
Struni-spec-collect-idents
Struct-declor-collect-idents
Struct-declon-collect-idents
Statassert-collect-idents
Spec/qual-list-collect-idents
Spec/qual-collect-idents
Param-declor-collect-idents
Param-declon-collect-idents
Member-designor-collect-idents
Initer-option-collect-idents
Initer-collect-idents
Init-declor-list-collect-idents
Init-declor-collect-idents
Genassoc-list-collect-idents
Genassoc-collect-idents
Expr-option-collect-idents
Expr-list-collect-idents
Enumer-list-collect-idents
Enum-spec-collect-idents
Dirdeclor-collect-idents
Dirabsdeclor-collect-idents
Desiniter-list-collect-idents
Desiniter-collect-idents
Designor-list-collect-idents
Designor-collect-idents
Declor-option-collect-idents
Declon-list-collect-idents
Decl-spec-list-collect-idents
Decl-spec-collect-idents
Const-expr-collect-idents
Comp-stmt-collect-idents
Block-item-list-collect-idents
Block-item-collect-idents
Attrib-spec-list-collect-idents
Attrib-spec-collect-idents
Attrib-list-collect-idents
Attrib-collect-idents
Asm-stmt-collect-idents
Asm-output-list-collect-idents
Asm-output-collect-idents
Asm-input-list-collect-idents
Asm-input-collect-idents
Amb-expr/tyname-collect-idents
Amb-declon/stmt-collect-idents
Align-spec-collect-idents
Absdeclor-option-collect-idents
Absdeclor-collect-idents
Tyname-collect-idents
Stmt-collect-idents
Label-collect-idents
Expr-collect-idents
Enumer-collect-idents
Declor-collect-idents
Declon-collect-idents
Subst-free
Proof-generation-theorems
Input-processing
Language
Representation
Insertion-sort
Pack
Soft
Bv
Imp-language
Ethereum
Event-macros
Java
Riscv
Bitcoin
Zcash
Yul
ACL2-programming-language
Prime-fields
Json
Syntheto
File-io-light
Cryptography
Number-theory
Axe
Lists-light
Builtins
Solidity
Helpers
Htclient
Typed-lists-light
Arithmetic-light
X86isa
Axe
Execloader
Math
Testing-utilities
Collect-idents
Abstract-syntax-collect-idents
Subtopics
Exprs/decls/stmts-collect-idents
Filepath-transunit-map-collect-idents
Transunit-ensemble-collect-idents
Ext-declon-list-collect-idents
Fundef-option-collect-idents
Ext-declon-collect-idents
Ident-option-collect-idents
Ident-list-collect-idents
Transunit-collect-idents
Fundef-collect-idents
Ident-collect-idents
Typequal/attribspec-list-list-collect-idents
Typequal/attribspec-list-collect-idents
Typequal/attribspec-collect-idents
Struct-declor-list-collect-idents
Struct-declon-list-collect-idents
Param-declon-list-collect-idents
Dirabsdeclor-option-collect-idents
Const-expr-option-collect-idents
Amb-declor/absdeclor-collect-idents
Type-spec-collect-idents
Struni-spec-collect-idents
Struct-declor-collect-idents
Struct-declon-collect-idents
Statassert-collect-idents
Spec/qual-list-collect-idents
Spec/qual-collect-idents
Param-declor-collect-idents
Param-declon-collect-idents
Member-designor-collect-idents
Initer-option-collect-idents
Initer-collect-idents
Init-declor-list-collect-idents
Init-declor-collect-idents
Genassoc-list-collect-idents
Genassoc-collect-idents
Expr-option-collect-idents
Expr-list-collect-idents
Enumer-list-collect-idents
Enum-spec-collect-idents
Dirdeclor-collect-idents
Dirabsdeclor-collect-idents
Desiniter-list-collect-idents
Desiniter-collect-idents
Designor-list-collect-idents
Designor-collect-idents
Declor-option-collect-idents
Declon-list-collect-idents
Decl-spec-list-collect-idents
Decl-spec-collect-idents
Const-expr-collect-idents
Comp-stmt-collect-idents
Block-item-list-collect-idents
Block-item-collect-idents
Attrib-spec-list-collect-idents
Attrib-spec-collect-idents
Attrib-list-collect-idents
Attrib-collect-idents
Asm-stmt-collect-idents
Asm-output-list-collect-idents
Asm-output-collect-idents
Asm-input-list-collect-idents
Asm-input-collect-idents
Amb-expr/tyname-collect-idents
Amb-declon/stmt-collect-idents
Align-spec-collect-idents
Absdeclor-option-collect-idents
Absdeclor-collect-idents
Tyname-collect-idents
Stmt-collect-idents
Label-collect-idents
Expr-collect-idents
Enumer-collect-idents
Declor-collect-idents
Declon-collect-idents