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
Software-verification
Kestrel-books
Crypto-hdwallet
Apt
Error-checking
Fty-extensions
Isar
Kestrel-utilities
Soft
Bv
Imp-language
C
Syntax-for-tools
Disambiguator
Abstract-syntax
Parser
Validator
Printer
Formalized-subset
Mapping-to-language-definition
Defpred
Output-files
Input-files
Abstract-syntax-operations
Validation-information
Type
Abstract-syntax-annop
Typequal/attribspec-list-list-annop
Typequal/attribspec-list-annop
Type-spec-list-annop
Extdecl-list-annop
Exprs/decls/stmts-annop
Structdeclor-list-annop
Attrib-spec-list-annop
Structdecl-list-annop
Initdeclor-list-annop
Block-item-list-annop
Asm-output-list-annop
Spec/qual-list-annop
Paramdecl-list-annop
Desiniter-list-annop
Decl-spec-list-annop
Asm-input-list-annop
Genassoc-list-annop
Designor-list-annop
Enumer-list-annop
Attrib-list-annop
Expr-list-annop
Decl-list-annop
Filepath-transunit-map-annop
Transunit-ensemble-annop
Declor/absdeclor-annop
Fundef-option-annop
Expr/tyname-annop
Transunit-annop
Fundef-annop
Extdecl-annop
Decl/stmt-annop
Typequal/attribspec-annop
Member-designor-annop
Initer-option-annop
Dirabsdeclor-option-annop
Declor-option-annop
Const-expr-option-annop
Amb-expr/tyname-annop
Amb-decl/stmt-annop
Amb-declor/absdeclor-annop
Absdeclor-option-annop
Type-spec-annop
Tyname-annop
Strunispec-annop
Structdeclor-annop
Structdecl-annop
Stmt-annop
Statassert-annop
Spec/qual-annop
Paramdeclor-annop
Paramdecl-annop
Label-annop
Initer-annop
Initdeclor-annop
Genassoc-annop
Expr-option-annop
Expr-annop
Enumspec-annop
Enumer-annop
Dirdeclor-annop
Dirabsdeclor-annop
Desiniter-annop
Designor-annop
Declor-annop
Decl-spec-annop
Decl-annop
Const-expr-annop
Block-item-annop
Attrib-spec-annop
Attrib-annop
Asm-stmt-annop
Asm-output-annop
Asm-input-annop
Align-spec-annop
Absdeclor-annop
Type-uaconvert-signed-unsigned
Type-uaconvert
Lifetime
Type-promote
Linkage-option
Linkage
Lifetime-option
Var-info
Type-option
Type-uaconvert-unsigned
Type-uaconvert-signed
Type-unsigned-integerp
Type-fpconvert
Type-signed-integerp
Type-promotedp
Type-arithmeticp
Type-apconvert
Type-standard-unsigned-integerp
Type-standard-signed-integerp
Type-aggregatep
Type-standard-integerp
Type-real-floatingp
Type-integerp
Type-floatingp
Type-complexp
Type-characterp
Type-basicp
Type-scalarp
Type-realp
Coerce-var-info
Irr-var-info
Type-set
Type-option-type-alist
Irr-linkage
Irr-lifetime
Type-list
Irr-type
Implementation-environments
Concrete-syntax
Unambiguity
Preprocessing
Abstraction-mapping
Atc
Language
Representation
Transformation-tools
Pack
Event-macros
Java
Bitcoin
Ethereum
Yul
Zcash
ACL2-programming-language
Prime-fields
Json
Syntheto
File-io-light
Number-theory
Cryptography
Lists-light
Builtins
Axe
Solidity
Helpers
Htclient
Typed-lists-light
Arithmetic-light
X86isa
Axe
Execloader
Math
Testing-utilities
Abstract-syntax-annop
Stmt-annop
Signature
(stmt-annop stmt) → yes/no
Arguments
stmt
—
Guard
(
stmtp
stmt)
.
Returns
yes/no
—
Type
(
booleanp
yes/no)
.