Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Debugging
Projects
Apt
Acre
Milawa
Smtlink
Abnf
Vwsim
Isar
Wp-gen
Dimacs-reader
Pfcs
Legacy-defrstobj
Proof-checker-array
Soft
Farray
Rp-rewriter
Instant-runoff-voting
Imp-language
Sidekick
Leftist-trees
C
Atc
Syntax-for-tools
Abstract-syntax
Expr
Exprs/decls
Binop
Abstract-syntax-operations
Expr-priority
Expr-priority-<=
Combine-dirabsdeclor-into-dirabsdeclor
Expr->priority
Check-declspec-list-all-tyspec/stoclaspec
Binop-expected-priorities
Check-expr-binary
Apply-post-inc/dec-ops
Apply-pre-inc/dec-ops
Check-specqual-list-all-tyspec
Check-expr-mul
Check-declspec-list-all-tyspec
Expr-to-asg-expr-list
Expr-unary/postfix/primary-p
Expr-zerop
Check-strunispec-no-members
Expr-postfix/primary-p
Dirabsdeclor-decl?-nil-p
Declspec-list-to-stoclaspec-list
Check-enumspec-no-list
Specqual-list-to-tyspec-list
Declspec-list-to-tyspec-list
Check-expr-iconst
Check-expr-ident
Declor->ident
Dirdeclor->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-stoclaspec
Irr-statassert
Irr-specqual
Irr-paramdeclor
Irr-paramdecl
Irr-initdeclor
Irr-hex-quad
Irr-expr/tyname
Irr-enumspec
Irr-dirdeclor
Irr-dirabsdeclor
Irr-desiniter
Irr-declspec
Irr-dec-expo-prefix
Irr-dec-expo
Irr-const-expr
Irr-bin-expo-prefix
Irr-bin-expo
Irr-attrib-spec
Irr-asm-name-spec
Irr-alignspec
Irr-absdeclor
Irr-unop
Irr-tyspec
Irr-tyqual
Irr-tyname
Irr-transunit
Irr-stmt
Irr-initer
Irr-ident
Irr-genassoc
Irr-funspec
Irr-extdecl
Irr-expr
Irr-escape
Irr-enumer
Irr-designor
Irr-declor
Irr-decl
Irr-const
Irr-block-item
Irr-binop
Irr-attrib
Tyspec
Amb-expr/tyname
Dirdeclor
Stmt
Unop
Dec/oct/hex-const
Attrib
Simple-escape
Dirabsdeclor
Decl
Amb-decl/stmt
Ident
Amb-declor/absdeclor
Tyqual
Asm-name-spec
Paramdeclor
Transunit-ensemble
Structdecl
Declor
Stoclaspec
Fundef
Alignspec
Lsuffix
Declspec
Hex-frac-const
Funspec
Dec-frac-const
Dec-core-fconst
Absdeclor
Strunispec
Expr-option
Dirabsdeclor-option
Desiniter
Amb?-declor/absdeclor
Isuffix
Hex-core-fconst
Escape
Amb?-expr/tyname
Structdeclor
Specqual
Label
Const-expr-option
Bin-expo
Tyname
Fsuffix
Enumspec
Absdeclor-option
Paramdecl
Initer-option
Declor-option
Const
Block-item
Oct-escape
Initer
Inc/dec-op
Iconst
Hex-quad
Eprefix
Dec-expo
Cprefix-option
Const-expr
Asm-name-spec-option
Amb?-decl/stmt
S-char
Isuffix-option
Ident-option
Fsuffix-option
Fconst
Eprefix-option
Dec-expo-option
Cprefix
C-char
Sign-option
Iconst-option
Genassoc
Const-option
Usuffix
Univ-char-name
Statassert
Designor
Sign
Hprefix
Stringlit
Initdeclor
Enumer
Dec-expo-prefix
Bin-expo-prefix
Extdecl
Cconst
Attrib-spec
Transunit
Expr/tyname
Declor/absdeclor
Inc/dec-op-list
Declspec-list
Tyqual-list
Specqual-list
S-char-list
Decl-list
C-char-list
Structdeclor-list
Structdecl-list
Paramdecl-list
Initdeclor-list
Genassoc-list
Extdecl-list
Desiniter-list
Stmts/blocks
File-paths
Enumer-list
Block-item-list
Tyqual-list-list
Stringlit-list
Filepath-transunit-map
Attrib-spec-list
Stoclaspec-list
Ident-list
Expr-list
Designor-list
Attrib-list
Tyspec-list
Parser
Printer
Mapping-to-language-definition
Read-files
Read-and-parse-files
Print-files
Parse-files
Concrete-syntax
Write-files
Print-and-write-files
Preprocessing
Language
Representation
Transformation-tools
Pack
Java
Taspi
Bitcoin
Des
Ethereum
Sha-2
Yul
Zcash
Proof-checker-itp13
Bigmem
Regex
ACL2-programming-language
Json
X86isa
Jfkr
Equational
Cryptography
Poseidon
Where-do-i-place-my-book
Builtins
Axe
Execloader
Solidity
Paco
Concurrent-programs
Std
Proof-automation
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
Software-verification
Math
Testing-utilities
Declor->ident
Dirdeclor->ident
Signature
(dirdeclor->ident dirdeclor) → ident
Arguments
dirdeclor
—
Guard
(
dirdeclorp
dirdeclor)
.
Returns
ident
—
Type
(
identp
ident)
.