Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Projects
Apt
Zfc
Acre
Milawa
Smtlink
Abnf
Vwsim
Isar
Wp-gen
Dimacs-reader
Pfcs
Legacy-defrstobj
Proof-checker-array
Soft
C
Farray
Rp-rewriter
Instant-runoff-voting
Imp-language
Sidekick
Leftist-trees
Java
Riscv
Taspi
Bitcoin
Des
Ethereum
X86isa
Sha-2
Yul
Zcash
Proof-checker-itp13
Regex
ACL2-programming-language
Json
Jfkr
Equational
Cryptography
Poseidon
Where-do-i-place-my-book
Axe
Aleo
Aleobft
Aleovm
Leo
Grammar
Early-version
Json2ast
Testing
Definition
Flattening
Abstract-syntax
Expression
Syntax-abstraction
Abs-*-hexadecimal-digit-to-nat
Abs-*-decimal-digit-to-nat
Chars+exprs
Abs-transition-declaration
Abs-not-double-quote-or-backslash-or-line-feed-or-carriage-return
Abs-named-type
Chars+exprs-result
Abs-*-lowercaseletter/decimaldigit
Abs-*-letter/decimaldigit/underscore
Abs-*-comma-struct-component-declaration
Abs-hexadecimal-digit-to-nat
Abs-assignment-operator
Abs-struct-component-declarations
Abs-lowercaseletter/decimaldigit
Abs-letter/decimaldigit/underscore
Abs-increment-statement
Abs-group-coordinate
Abs-function-parameter
Abs-function-declaration
Abs-decrement-statement
Abs-unsigned-literal
Abs-record-declaration
Abs-mapping-declaration
Abs-variable-declaration
Abs-signed-literal
Abs-constant-declaration
Abs-*-comma-function-parameter
Abs-unicode-character-escape
Abs-struct-declaration
Abs-struct-component-declaration
Abs-simple-character-escape
Abs-finalizer
Abs-decimal-digit-to-nat
Abs-comma-struct-component-declaration
Abs-affine-group-literal
Check-literal-is-string-literal
Abs-*-annotation
Abs-variable-or-free-constant
Abs-string-literal-element
Abs-program-item
Abs-program-declaration
Abs-print-arguments
Abs-octal-digit-to-nat
Abs-finalize-statement
Abs-declaration
Abs-decimal-digit-to-char
Abs-console-statement
Abs-assignment-statement
Abs-ascii-character-escape
*binary-opcall-name-to-binop*
Abs-?-function-parameters
Abs-*-string-literal-element
Abs-*-import-declaration
Abs-uppercase-letter
Abs-unsigned-type
Abs-signed-type
Abs-return-statement
Abs-product-group-literal
Abs-print-call
Abs-named-primitive-type
Abs-lowercase-letter
Abs-import-declaration
Abs-identifier
Abs-function-parameters
Abs-comma-function-parameter
Abs-?-output-type
Abs-*-declaration
Abs-unit-expression
Abs-string-literal
Abs-program-id
Abs-numeric-literal
Abs-letter
Abs-integer-literal
Abs-double-quote-escape
Abs-carriage-return-escape
Abs-boolean-literal
Abs-atomic-literal
Abs-assert-call
Abs-arithmetic-type
Abs-address-literal
Check-optional-equals-p
Abs-?-finalizer
Abs-*-program-item
Abs-scalar-literal
Abs-null-character-escape
Abs-locator
Abs-integer-type
Abs-horizontal-tab-escape
Abs-field-literal
Abs-console-call
Abs-backslash-escape
Abs-annotation
Check-?-comma
Abs-unit-type
Abs-string-type
Abs-scalar-type
Abs-literal
Abs-line-feed-escape
Abs-double-quote
Abs-boolean-type
Abs-address-type
Empty-optional-tree-p
Abs-numeral
Abs-group-type
Abs-file
Abs-field-type
Unop-for-opcall-name
Binop-for-opcall-name
Abs-safe-nonascii
*unary-opcall-name-to-unop*
Abs-?-expression-*-comma-expression-?-comma
Abs-*-comma-struct-component-initializer
Abs-1*-comma-expression
Abs-*-statement
Abs-*-comma-type
Abs-*-comma-expression
Abs-unary-operator-call
Abs-unary-expression
Abs-tuple-expression
Abs-tuple-component-expression
Abs-struct-expression
Abs-struct-component-initializer
Abs-struct-component-expression
Abs-shift-expression
Abs-primary-expression
Abs-postfix-expression
Abs-ordering-expression
Abs-multiplicative-expression
Abs-function-arguments
Abs-free-function-call
Abs-exponential-expression
Abs-exclusive-disjunctive-expression
Abs-equality-expression
Abs-disjunctive-expression
Abs-conjunctive-expression
Abs-conditional-ternary-expression
Abs-conditional-statement
Abs-conditional-disjunctive-expression
Abs-conditional-conjunctive-expression
Abs-comma-struct-component-initializer
Abs-comma-expression
Abs-block
Abs-binary-operator-call
Abs-binary-expression
Abs-additive-expression
Abs-1*-comma-type
Abs-type
Abs-tuple-type
Abs-statement
Abs-operator-call
Abs-loop-statement
Abs-expression
Abs-comma-type
Abs-branch
Statement
Files
Input-files
Identifiers
Types
Struct-init
Branch
Statements
Format-strings
Input-syntax-abstraction
Expressions
Output-files
Addresses
Literals
Characters
Expression-list
Statement-list
Output-syntax-abstraction
Struct-init-list
Branch-list
Annotations
Abstract-syntax-trees
Symbols
Keywords
Programs
Packages
Bit-sizes
Dynamic-semantics
Compilation
Static-semantics
Concrete-syntax
Bigmems
Builtins
Execloader
Solidity
Paco
Concurrent-programs
Bls12-377-curves
Debugging
Community
Std
Proof-automation
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
Software-verification
Math
Testing-utilities
Syntax-abstraction
Abs-statement
Abstract a
statement
to a statement.
Signature
(abs-statement tree) → stat
Arguments
tree
—
Guard
(
abnf::treep
tree)
.
Returns
stat
—
Type
(
statement-resultp
stat)
.