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
Soft
C
Syntax-for-tools
Disambiguator
Abstract-syntax
Parser
Validator
Printer
Formalized-subset
Mapping-to-language-definition
Input-files
Defpred
Output-files
Abstract-syntax-operations
Validation-information
Implementation-environments
Concrete-syntax
Ascii-identifiers
Abstract-syntax-aidentp
Exprs/decls/stmts-aidentp
Filepath-transunit-map-aidentp
Extdecl-list-aidentp
Transunit-ensemble-aidentp
Ident-list-aidentp
Ident-option-aidentp
Attrib-name-aidentp
Transunit-aidentp
Fundef-aidentp
Extdecl-aidentp
Const-aidentp
Ident-aidentp
Typequal/attribspec-list-list-aidentp
Typequal/attribspec-list-aidentp
Structdeclor-list-aidentp
Structdecl-list-aidentp
Param-declon-list-aidentp
Initdeclor-list-aidentp
Block-item-list-aidentp
Attrib-spec-list-aidentp
Asm-output-list-aidentp
Spec/qual-list-aidentp
Genassoc-list-aidentp
Enumer-list-aidentp
Desiniter-list-aidentp
Designor-list-aidentp
Decl-spec-list-aidentp
Attrib-list-aidentp
Asm-input-list-aidentp
Expr-list-aidentp
Decl-list-aidentp
Typequal/attribspec-aidentp
Struni-spec-aidentp
Structdeclor-aidentp
Structdecl-aidentp
Statassert-aidentp
Param-declor-aidentp
Param-declon-aidentp
Member-designor-aidentp
Initer-option-aidentp
Initdeclor-aidentp
Expr-option-aidentp
Dirabsdeclor-option-aidentp
Dirabsdeclor-aidentp
Declor-option-aidentp
Const-expr-option-aidentp
Const-expr-aidentp
Block-item-aidentp
Attrib-spec-aidentp
Asm-output-aidentp
Amb-expr/tyname-aidentp
Amb-decl/stmt-aidentp
Amb-declor/absdeclor-aidentp
Align-spec-aidentp
Absdeclor-option-aidentp
Type-spec-aidentp
Tyname-aidentp
Stmt-aidentp
Spec/qual-aidentp
Label-aidentp
Initer-aidentp
Genassoc-aidentp
Expr-aidentp
Enumspec-aidentp
Enumer-aidentp
Dirdeclor-aidentp
Desiniter-aidentp
Designor-aidentp
Declor-aidentp
Decl-spec-aidentp
Decl-aidentp
Attrib-aidentp
Asm-stmt-aidentp
Asm-input-aidentp
Absdeclor-aidentp
Ascii-ident-stringp
Unambiguity
Preprocessing
Abstraction-mapping
Standard
Purity
Atc
Language
Transformation-tools
Representation
Insertion-sort
Pack
Bv
Imp-language
Event-macros
Java
Riscv
Bitcoin
Ethereum
Yul
Zcash
ACL2-programming-language
Prime-fields
Json
Syntheto
File-io-light
Cryptography
Number-theory
Lists-light
Axe
Builtins
Solidity
Helpers
Htclient
Typed-lists-light
Arithmetic-light
X86isa
Axe
Execloader
Math
Testing-utilities
Abstract-syntax-aidentp
Label-aidentp
Signature
(label-aidentp label gcc) → fty::result
Arguments
label
—
Guard
(
labelp
label)
.
gcc
—
Guard
(
booleanp
gcc)
.
Returns
fty::result
—
Type
(
booleanp
fty::result)
.