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
Formalized-subset
Mapping-to-language-definition
Input-files
Compilation-database
Printer
Output-files
Abstract-syntax-operations
Implementation-environments
Abstract-syntax
Concrete-syntax
Disambiguation
Validation
Validator
Validation-information
Abstract-syntax-annop
Exprs/decls/stmts-annop
Filepath-transunit-map-annop
Transunit-ensemble-annop
Code-ensemble-annop
Ident-option-annop
Iconst-option-annop
Extdecl-list-annop
Const-option-annop
Transunit-annop
Ident-list-annop
Attrib-name-annop
Fundef-annop
Extdecl-annop
Iconst-annop
Const-annop
Ident-annop
Typequal/attribspec-list-list-annop
Typequal/attribspec-list-annop
Typequal/attribspec-annop
Struni-spec-annop
Struct-declor-list-annop
Struct-declor-annop
Struct-declon-list-annop
Struct-declon-annop
Statassert-annop
Spec/qual-list-annop
Spec/qual-annop
Param-declor-annop
Param-declon-list-annop
Param-declon-annop
Member-designor-annop
Initer-option-annop
Initdeclor-list-annop
Initdeclor-annop
Genassoc-list-annop
Expr-option-annop
Enumer-list-annop
Dirabsdeclor-option-annop
Dirabsdeclor-annop
Desiniter-list-annop
Designor-list-annop
Declor-option-annop
Decl-spec-list-annop
Const-expr-option-annop
Const-expr-annop
Block-item-list-annop
Block-item-annop
Attrib-spec-list-annop
Attrib-spec-annop
Attrib-list-annop
Asm-output-list-annop
Asm-output-annop
Asm-input-list-annop
Amb-expr/tyname-annop
Amb-decl/stmt-annop
Amb-declor/absdeclor-annop
Align-spec-annop
Absdeclor-option-annop
Type-spec-annop
Tyname-annop
Stmt-annop
Label-annop
Initer-annop
Genassoc-annop
Expr-list-annop
Expr-annop
Enumer-annop
Enum-spec-annop
Dirdeclor-annop
Desiniter-annop
Designor-annop
Declor-annop
Decl-spec-annop
Decl-list-annop
Decl-annop
Comp-stmt-annop
Attrib-annop
Asm-stmt-annop
Asm-input-annop
Absdeclor-annop
Types
Abstract-syntax-anno-additional-theroems
Valid-ext-info
Valid-table
Valid-ord-info
Uid
Stmts-types
Lifetime
Initdeclor-info
Fundef-types
Expr-type
Valid-defstatus
Var-info
Valid-ord-info-option
Valid-ext-info-option
Uid-option
Linkage-option
Linkage
Lifetime-option
Valid-table-option
Iconst-info
Param-declor-nonabstract-info
Fundef-info
Expr-null-pointer-constp
Valid-scope
Const-expr-null-pointer-constp
Expr-string-info
Expr-funcall-info
Expr-arrsub-info
Tyname-info
Transunit-info
Expr-unary-info
Expr-const-info
Expr-binary-info
Stmt-types
Block-item-list-types
Initer-type
Valid-ord-scope
Uid-increment
Uid-equal
Coerce-var-info
Valid-externals
Irr-var-info
Valid-scope-list
Irr-valid-table
Irr-lifetime
Irr-uid
Irr-linkage
Block-item-types
Comp-stmt-types
Gcc-builtins
Preprocessing
Parsing
Atc
Transformation-tools
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
Abstract-syntax-annop
Block-item-list-annop
Signature
(block-item-list-annop block-item-list) → fty::result
Arguments
block-item-list
—
Guard
(
block-item-listp
block-item-list)
.
Returns
fty::result
—
Type
(
booleanp
fty::result)
.