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
Disambiguator
Unambiguity
Abstract-syntax-unambp
Exprs/decls/stmts-unambp
Filepath-transunit-map-unambp
Transunit-ensemble-unambp
Declor/absdeclor-unambp
Type-spec-list-unambp
Fundef-option-unambp
Extdecl-list-unambp
Expr/tyname-unambp
Code-ensemble-unambp
Fundef-unambp
Extdecl-unambp
Decl/stmt-unambp
Transunit-unambp
Typequal/attribspec-list-unambp
Typequal/attribspec-list-list-unambp
Typequal/attribspec-unambp
Struni-spec-unambp
Struct-declor-unambp
Struct-declor-list-unambp
Struct-declon-unambp
Struct-declon-list-unambp
Statassert-unambp
Spec/qual-unambp
Spec/qual-list-unambp
Param-declor-unambp
Param-declon-unambp
Param-declon-list-unambp
Member-designor-unambp
Initer-option-unambp
Initdeclor-unambp
Initdeclor-list-unambp
Genassoc-list-unambp
Expr-option-unambp
Enumer-list-unambp
Dirabsdeclor-unambp
Dirabsdeclor-option-unambp
Desiniter-list-unambp
Designor-list-unambp
Declor-option-unambp
Decl-spec-list-unambp
Const-expr-unambp
Const-expr-option-unambp
Block-item-unambp
Block-item-list-unambp
Attrib-spec-unambp
Attrib-spec-list-unambp
Attrib-list-unambp
Asm-output-unambp
Asm-output-list-unambp
Asm-input-list-unambp
Amb-expr/tyname-unambp
Amb-decl/stmt-unambp
Amb-declor/absdeclor-unambp
Align-spec-unambp
Absdeclor-option-unambp
Type-spec-unambp
Tyname-unambp
Stmt-unambp
Label-unambp
Initer-unambp
Genassoc-unambp
Expr-unambp
Expr-list-unambp
Enumer-unambp
Enum-spec-unambp
Dirdeclor-unambp
Desiniter-unambp
Designor-unambp
Declor-unambp
Decl-unambp
Decl-spec-unambp
Decl-list-unambp
Comp-stmt-unambp
Attrib-unambp
Asm-stmt-unambp
Asm-input-unambp
Absdeclor-unambp
Abstract-syntax-unambp-additional-theorems
Type-spec-list-unambp-of-sublists
Expr-unambp-of-operation-on-expr-unambp
Validation
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-unambp
Dirabsdeclor-option-unambp
Signature
(dirabsdeclor-option-unambp dirabsdeclor-option) → fty::result
Arguments
dirabsdeclor-option
—
Guard
(
dirabsdeclor-optionp
dirabsdeclor-option)
.
Returns
fty::result
—
Type
(
booleanp
fty::result)
.