Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Debugging
Projects
Std
Proof-automation
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
Software-verification
Kestrel-books
Crypto-hdwallet
Apt
Error-checking
Abnf
Fty-extensions
Isar
Kestrel-utilities
Soft
Bv
Imp-language
Event-macros
C
Atc
Syntax-for-tools
Disambiguator
Abstract-syntax
Expr
Exprs/decls/stmts
Type-spec
Binop
Stmt
Unambiguity
Abstract-syntax-operations
Expr-priority
Expr-priority-<=
Combine-dirabsdeclor-into-dirabsdeclor
Expr->priority
Binop-expected-priorities
Check-declspec-list-all-tyspec/storspec
Transunit-at-path
Check-expr-binary
Apply-post-inc/dec-ops
Check-spec/qual-list-all-tyspec
Check-declspec-list-all-tyspec
Apply-pre-inc/dec-ops
Check-expr-mul
Expr-to-asg-expr-list
Transunit-ensemble-paths
Expr-unary/postfix/primary-p
Expr-postfix/primary-p
Check-strunispec-no-members
Expr-zerop
Dirabsdeclor-decl?-nil-p
Spec/qual-list-to-type-spec-list
Declspec-list-to-type-spec-list
Declspec-list-to-stor-spec-list
Check-enumspec-no-list
Check-expr-iconst
Check-expr-ident
Declor->ident
Irr-amb?-declor/absdeclor
Irr-transunit-ensemble
Irr-declor/absdeclor
Irr-amb?-expr/tyname
Irr-amb?-decl/stmt
Irr-strunispec
Irr-structdeclor
Irr-structdecl
Irr-stringlit
Irr-stor-spec
Irr-statassert
Irr-spec/qual
Irr-paramdeclor
Irr-paramdecl
Irr-member-designor
Irr-initdeclor
Irr-hex-quad
Irr-fundef
Irr-expr/tyname
Irr-enumspec
Irr-dirdeclor
Irr-dirabsdeclor
Irr-desiniter
Irr-decl/stmt
Irr-declspec
Irr-dec-expo-prefix
Irr-dec-expo
Irr-const-expr
Irr-bin-expo-prefix
Irr-bin-expo
Irr-attrib-spec
Irr-attrib-name
Irr-asm-output
Irr-asm-name-spec
Irr-asm-input
Irr-asm-clobber
Irr-align-spec
Irr-absdeclor
Irr-unop
Irr-type-spec
Irr-type-qual
Irr-tyname
Irr-transunit
Irr-stmt
Irr-label
Irr-initer
Irr-ident
Irr-genassoc
Irr-fun-spec
Irr-extdecl
Irr-expr
Irr-escape
Irr-enumer
Irr-designor
Irr-declor
Irr-decl
Irr-const
Irr-block-item
Irr-binop
Irr-attrib
Irr-asm-qual
Amb-expr/tyname
Dirdeclor
Unop
Dec/oct/hex-const
Simple-escape
Attrib
Amb-decl/stmt
Dirabsdeclor
Ident
Asm-name-spec
Amb-declor/absdeclor
Transunit-ensemble
Paramdeclor
Type-qual
Structdecl
Fundef
Declspec
Declor
Decl
Absdeclor
Stor-spec
Keyword-uscores
Attrib-name
Align-spec
Lsuffix
Label
Spec/qual
Hex-frac-const
Expr-option
Dec-frac-const
Dec-core-fconst
Strunispec
Dirabsdeclor-option
Desiniter
Amb?-declor/absdeclor
Tyname
Isuffix
Hex-core-fconst
Escape
Const-expr-option
Attrib-spec
Amb?-expr/tyname
Structdeclor
Bin-expo
Statassert
Fsuffix
Enumspec
Absdeclor-option
Paramdecl
Member-designor
Initer-option
Initer
Ident-option
Declor-option
Const
Block-item
Oct-escape
Inc/dec-op
Iconst
Hex-quad
Fun-spec
Extdecl
Eprefix
Dec-expo
Cprefix-option
Const-expr
Asm-name-spec-option
Amb?-decl/stmt
S-char
Isuffix-option
Fsuffix-option
Fconst
Eprefix-option
Dec-expo-option
Cprefix
C-char
Sign-option
Iconst-option
Genassoc
Fundef-option
Asm-output
Asm-input
Initdeclor
Const-option
Usuffix
Univ-char-name
Designor
Sign
Hprefix
Asm-qual
Enumer
Dec-expo-prefix
Bin-expo-prefix
Stringlit
Cconst
Transunit
Expr/tyname
Decl/stmt
Declor/absdeclor
Asm-clobber
Abstraction-mapping
Type-qual-list
Stringlit-list
Spec/qual-list
Inc/dec-op-list
Declspec-list
S-char-list
Decl-list
C-char-list
Structdeclor-list
Structdecl-list
Paramdecl-list
Initdeclor-list
Genassoc-list
Extdecl-list
Desiniter-list
File-paths
Enumer-list
Block-item-list
Type-qual-list-list
Ident-list
Filepath-transunit-map
Expr-list
Attrib-spec-list
Asm-qual-list
Asm-output-list
Asm-input-list
Asm-clobber-list
Type-spec-list
Stor-spec-list
Ident-set
Ident-option-set
Designor-list
Attrib-list
Parser
Printer
Formalized-subset
Mapping-to-language-definition
Output-files
Input-files
Validator
Implementation-environments
Concrete-syntax
Preprocessing
Language
Representation
Transformation-tools
Pack
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
Abstract-syntax-operations
Operations on the abstract syntax.
Subtopics
Expr-priority
Fixtype of expression priorities.
Expr-priority-<=
Total order on expression priorities.
Combine-dirabsdeclor-into-dirabsdeclor
Combine a direct abstract declarator into another.
Expr->priority
Priorities of expressions.
Binop-expected-priorities
Expected expression priorities of the operands of the binary operators.
Check-declspec-list-all-tyspec/storspec
Check if all the declaration specifiers in a list are type specifiers or storage class specifiers.
Transunit-at-path
Translation unit at a certain path in a translation unit ensemble.
Check-expr-binary
Check if an expression is a binary expression.
Apply-post-inc/dec-ops
Apply a sequence of post-increment and post-decrement operators to an expression.
Check-spec/qual-list-all-tyspec
Check if all the specifiers and qualifiers in a list are type specifiers.
Check-declspec-list-all-tyspec
Check if all the declaration specifiers in a list are type specifiers.
Apply-pre-inc/dec-ops
Apply a sequence of pre-increment and pre-decrement operators to an expression.
Check-expr-mul
Check if an expression is a multiplication.
Expr-to-asg-expr-list
Turn an expression into a list of assignment expressions.
Transunit-ensemble-paths
Set of file paths in a translation unit ensemble.
Expr-unary/postfix/primary-p
Check if an expression is unary or postfix or primary.
Expr-postfix/primary-p
Check if an expression is postfix or primary.
Check-strunispec-no-members
Check if a structure or union specifier has no members, returning the name if the check passes.
Expr-zerop
Check if an expression is zero.
Dirabsdeclor-decl?-nil-p
Check if a direct abstract declarator has a
decl?
component that is
nil
.
Spec/qual-list-to-type-spec-list
Extract the list of type specifiers from a list of type specifiers and qualifiers, preserving the order.
Declspec-list-to-type-spec-list
Extract the list of type specifiers from a list of declaration specifiers, preserving the order.
Declspec-list-to-stor-spec-list
Extract the list of storage class specifiers from a list of declaration specifiers, preserving the order.
Check-enumspec-no-list
Check if an enumeration union specifier has no enumerators, returning the name if the check passes.
Check-expr-iconst
Check if an expression is an integer constant, returning the integer constant if the check passes.
Check-expr-ident
Check if an expression is an identifier, returning the identifier if the check passes.
Declor->ident
Identifier of a declarator.
Irr-amb?-declor/absdeclor
An irrelevant possibly ambiguous declarators or abstract declarators.
Irr-transunit-ensemble
An irrelevant ensemble of translation units.
Irr-declor/absdeclor
An irrelevant declarator or abstract declarator.
Irr-amb?-expr/tyname
An irrelevant possibly ambiguous expression or type name.
Irr-amb?-decl/stmt
An irrelevant possibly ambiguous declaration or statement.
Irr-strunispec
An irrelevant structure or union specifier.
Irr-structdeclor
An irrelevant structure declarator.
Irr-structdecl
An irrelevant structure declaration.
Irr-stringlit
An irrelevant string literal.
Irr-stor-spec
An irrelevant storage class specifier.
Irr-statassert
An irrelevant static assertion declaration.
Irr-spec/qual
An irrelevant type specifier or type qualifier.
Irr-paramdeclor
An irrelevant parameter declarator.
Irr-paramdecl
An irrelevant parameter declaration.
Irr-member-designor
An irrelevant member designator.
Irr-initdeclor
An irrelevant initializer declarator.
Irr-hex-quad
An irrelevant quadruple of hexadecimal digits.
Irr-fundef
An irrelevant function definition.
Irr-expr/tyname
An irrelevant expression or type name.
Irr-enumspec
An irrelevant enumeration specifier.
Irr-dirdeclor
An irrelevant direct declarator.
Irr-dirabsdeclor
An irrelevant direct abstract declarator.
Irr-desiniter
An irrelevant initializer with optional designation.
Irr-decl/stmt
An irrelevant declaration or statement.
Irr-declspec
An irrelevant declaration specifier.
Irr-dec-expo-prefix
An irrelevant decimal exponent prefix.
Irr-dec-expo
An irrelevant decimal exponent.
Irr-const-expr
An irrelevant constant expression.
Irr-bin-expo-prefix
An irrelevant binary exponent prefix.
Irr-bin-expo
An irrelevant binary exponent.
Irr-attrib-spec
An irrelevant attribute specifier.
Irr-attrib-name
An irrelevant attribute name.
Irr-asm-output
An irrelevant assembler output operand.
Irr-asm-name-spec
An irrelevant assembler name specifier.
Irr-asm-input
An irrelevant assembler input operand.
Irr-asm-clobber
An irrelevant assembler clobber.
Irr-align-spec
An irrelevant alignment specifier.
Irr-absdeclor
An irrelevant abstract declarator.
Irr-unop
An irrelevant unary operator.
Irr-type-spec
An irrelevant type specifier.
Irr-type-qual
An irrelevant type qualifier.
Irr-tyname
An irrelevant type name.
Irr-transunit
An irrelevant translation unit.
Irr-stmt
An irrelevant statement.
Irr-label
An irrelevant label.
Irr-initer
An irrelevant initializer.
Irr-ident
An irrelevant identifier.
Irr-genassoc
An irrelevant generic association.
Irr-fun-spec
An irrelevant function specifier.
Irr-extdecl
An irrelevant external declaration.
Irr-expr
An irrelevant expression.
Irr-escape
An irrelevant escape.
Irr-enumer
An irrelevant enumerator.
Irr-designor
An irrelevant designator.
Irr-declor
An irrelevant declarator.
Irr-decl
An irrelevant declaration.
Irr-const
An irrelevant constant.
Irr-block-item
An irrelevant block item.
Irr-binop
An irrelevant binary operator.
Irr-attrib
An irrelevant attribute.
Irr-asm-qual
An irrelevant assembler qualifier.