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
Set
Soft
C
Syntax-for-tools
Disambiguator
Abstract-syntax
Parser
Validator
Printer
Formalized-subset
Mapping-to-language-definition
Input-files
Validation-information
Type
Abstract-syntax-annop
Exprs/decls/stmts-annop
Filepath-transunit-map-annop
Transunit-ensemble-annop
Extdecl-list-annop
Ident-list-annop
Ident-option-annop
Iconst-option-annop
Const-option-annop
Transunit-annop
Fundef-annop
Attrib-name-annop
Extdecl-annop
Iconst-annop
Const-annop
Typequal/attribspec-list-list-annop
Ident-annop
Typequal/attribspec-list-annop
Structdeclor-list-annop
Structdecl-list-annop
Spec/qual-list-annop
Paramdecl-list-annop
Initdeclor-list-annop
Genassoc-list-annop
Enumer-list-annop
Desiniter-list-annop
Designor-list-annop
Decl-spec-list-annop
Block-item-list-annop
Attrib-spec-list-annop
Attrib-list-annop
Asm-output-list-annop
Asm-input-list-annop
Expr-list-annop
Decl-list-annop
Typequal/attribspec-annop
Strunispec-annop
Structdeclor-annop
Structdecl-annop
Statassert-annop
Spec/qual-annop
Paramdeclor-annop
Member-designor-annop
Initer-option-annop
Initdeclor-annop
Expr-option-annop
Dirabsdeclor-option-annop
Dirabsdeclor-annop
Declor-option-annop
Const-expr-option-annop
Const-expr-annop
Block-item-annop
Attrib-spec-annop
Asm-output-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
Paramdecl-annop
Label-annop
Initer-annop
Genassoc-annop
Expr-annop
Enumspec-annop
Enumer-annop
Dirdeclor-annop
Desiniter-annop
Designor-annop
Declor-annop
Decl-spec-annop
Decl-annop
Attrib-annop
Asm-stmt-annop
Asm-input-annop
Absdeclor-annop
Type-compatiblep
Type-uaconvert-signed-unsigned
Type-uaconvert
Valid-ord-info
Lifetime
Type-promote
Valid-defstatus
Valid-table
Valid-ord-info-option
Linkage-option
Linkage
Lifetime-option
Iconst-info
Var-info
Type-option
Valid-scope
Type-uaconvert-unsigned
Expr-null-pointer-constp
Type-uaconvert-signed
Transunit-info
Expr-type
Const-expr-null-pointer-constp
Unary-info
Binary-info
Type-unsigned-integerp
Type-fpconvert
Type-signed-integerp
Type-promotedp
Type-arithmeticp
Type-apconvert
Valid-ord-scope
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-transunit-info
Coerce-var-info
Coerce-unary-info
Coerce-iconst-info
Coerce-binary-info
Irr-transunit-info
Irr-iconst-info
Irr-binary-info
Irr-var-info
Irr-valid-table
Irr-unary-info
Valid-scope-list
Type-set
Type-option-type-alist
Irr-linkage
Irr-lifetime
Type-list
Irr-type
Defpred
Output-files
Abstract-syntax-operations
Implementation-environments
Concrete-syntax
Unambiguity
Ascii-identifiers
Preprocessing
Abstraction-mapping
Atc
Language
Representation
Transformation-tools
Insertion-sort
Pack
Bv
Imp-language
Event-macros
Java
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-annop
Expr-annop
Signature
(expr-annop expr) → fty::result
Arguments
expr
—
Guard
(
exprp
expr)
.
Returns
fty::result
—
Type
(
booleanp
fty::result)
.
