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
Defpred
Output-files
Abstract-syntax-operations
Abstract-syntax-irrelevants
Expr-priority
Expr-priority-<=
Combine-dirabsdeclor-into-dirabsdeclor
Check-decl-spec-list-all-typespec/stoclass
Binop-expected-priorities
Expr->priority
Transunit-at-path
Check-expr-binary
Apply-pre-inc/dec-ops
Apply-post-inc/dec-ops
Check-spec/qual-list-all-typespec
Check-decl-spec-list-all-typespec
Check-expr-mul
Type-spec-list-signed-long-long-int-p
Expr-unary/postfix/primary-p
Expr-to-asg-expr-list
Transunit-ensemble-paths
Type-spec-list-signed-short-int-p
Type-spec-list-signed-long-long-p
Type-spec-list-signed-long-int-p
Expr-postfix/primary-p
Dirabsdeclor-declor?-nil-p
Check-strunispec-no-members
Type-spec-list-signed-short-p
Type-spec-list-signed-long-p
Type-spec-list-signed-int128-p
Type-spec-list-signed-char-p
Expr-zerop
Type-spec-list-unsigned-long-long-int-p
Type-spec-list-signed-int-p
Spec/qual-list-to-type-spec-list
Expr-priority->=
Expr-priority->
Expr-priority-<
Decl-spec-list-to-type-spec-list
Decl-spec-list-to-stor-spec-list
Check-enumspec-no-list
Type-spec-list-unsigned-short-int-p
Type-spec-list-unsigned-long-long-p
Type-spec-list-long-double-complex-p
Stor-spec-list-static-threadloc-p
Stor-spec-list-extern-threadloc-p
Binop->priority
Type-spec-list-unsigned-short-p
Type-spec-list-unsigned-long-int-p
Type-spec-list-unsigned-int128-p
Type-spec-list-signed-p
Type-spec-list-long-long-int-p
Type-spec-list-double-complex-p
Type-spec-list-unsigned-long-p
Type-spec-list-unsigned-int-p
Type-spec-list-unsigned-char-p
Type-spec-list-long-double-p
Type-spec-list-float-complex-p
Type-spec-list-short-int-p
Type-spec-list-long-long-p
Type-spec-list-long-int-p
Stringlit-list->prefix?-list
Stor-spec-list-typedef-p
Stor-spec-list-threadloc-p
Stor-spec-list-static-p
Stor-spec-list-register-p
Stor-spec-list-extern-p
Type-spec-list-unsigned-p
Type-spec-list-short-p
Type-spec-list-long-p
Type-spec-list-int128-p
Type-spec-list-float-p
Type-spec-list-double-p
Type-spec-list-char-p
Stor-spec-list-auto-p
Check-expr-iconst
Type-spec-list-int-p
Check-expr-ident
Declor->ident
Dirdeclor->ident
Type-spec-list-permp
Initdeclor->ident
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
Declor->ident
Dirdeclor->ident
Signature
(dirdeclor->ident dirdeclor) → ident
Arguments
dirdeclor
—
Guard
(
dirdeclorp
dirdeclor)
.
Returns
ident
—
Type
(
identp
ident)
.