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
Dynamic-semantics
Compilation
Static-semantics
Concrete-syntax
Pretty-printer
Grammar
Lexing-and-parsing
Lexer
Parser
Parse-symbol-among
Parse-keyword
Parse-named-primitive-type
Parse-rest-of-struct-component-expression
Parse-rest-of-tuple-component-expression
Parse-transition-declaration
Parse-named-type-as-identifier-?-dot-record
Parse-named-type-as-locator-?-dot-record
Parse-assert-not-equal-call
Parse-symbol
Parse-struct-component-declarations
Parse-assert-equal-call
Parse-transition-or-function-declaration
Parse-string-literal
Parse-group-coordinate
Parse-function-declaration
Parse-finalizer
Parse-*-comma-struct-component-declaration
Parse-increment-statement
Parse-function-parameter
Parse-decrement-statement
Parse-struct-component-declaration
Parse-variable-declaration
Parse-mapping-declaration
Parse-function-parameters
Parse-constant-declaration
Parse-assert-call
Parse-*-comma-function-parameter
Parse-program-declaration
Parse-affine-group-literal
Parse-variable-or-free-constant
Parse-struct-declaration
Parse-record-declaration
Parse-finalize-statement
Parse-associated-constant
Parse-numeral
Parse-import-declaration
Parse-identifier
Parse-console-statement
Parse-annotation
Parse-return-statement
Parse-program-item
Parse-assignment-operator
Parse-*-import-declaration
Parse-unit-expression
Parse-named-type
Parse-console-call
Parse-*-comma-natural
Parse-program-id
Parse-atomic-literal
Parse-?-output-type
Parse-unit-type
Parse-*-program-item
Parse-locator
Parse-?-finalizer
Parse-*-annotation
Parse-primary-expression
Parse-literal
Parse-?-comma
Parse-file
Parsize
Check-token-string
Check-token-root
Parse-postfix-expression-rest
Parse-postfix-expression
Parse-token
Token-stringp
Token-rootp
Patbind-pok<
Parse-rest-of-operator-call
Parse-exclusive-disjunctive-expression-rest
Parse-conditional-disjunctive-expression-rest
Parse-conditional-conjunctive-expression-rest
Parse-shift-expression-rest
Parse-multiplicative-expression-rest
Parse-disjunctive-expression-rest
Parse-conjunctive-expression-rest
Parse-additive-expression-rest
Parse-*-statement
Parse-*-comma-type
Parse-*-comma-struct-component-initializer
Parse-*-comma-expression
Parse-unary-expression
Parse-tuple-expression
Parse-struct-expression
Parse-struct-component-initializer
Parse-static-function-call
Parse-shift-expression
Parse-ordering-expression
Parse-multiplicative-expression
Parse-function-arguments
Parse-free-function-call
Parse-exponential-expression
Parse-exclusive-disjunctive-expression
Parse-equality-expression
Parse-disjunctive-expression
Parse-conjunctive-expression
Parse-conditional-ternary-expression
Parse-conditional-statement
Parse-conditional-disjunctive-expression
Parse-conditional-conjunctive-expression
Parse-binary-expression
Parse-additive-expression
Parse-type
Parse-tuple-type
Parse-statement
Parse-loop-statement
Parse-expression
Parse-branch
Parse-block
Patbind-pok
Perr
Token-fringe
Longest-lexp
Parser-interface
Grammar-lexp
Identifier-lexp
Output-file-parsep
Input-file-parsep
File-lex-parse-p
Filter-tokens
Lexp
File-parsep
Input-parser
Output-file-lex-parse-p
Input-file-lex-parse-p
Parser-abstractor-interface
Identifier-abnf-stringp
Symbol-abnf-stringp
Keyword-abnf-stringp
Output-parser
Tokenizer
Input-pretty-printer
Output-pretty-printer
Unicode-characters
Concrete-syntax-trees
Symbols
Keywords
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
Parser
Parse-block
Parse a
block
.
Signature
(parse-block token input) → (mv tree next-token rest-input)
Arguments
token
—
Guard
(
abnf::tree-optionp
token)
.
input
—
Guard
(
abnf::tree-listp
input)
.
Returns
tree
—
Type
(
abnf::tree-resultp
tree)
.
next-token
—
Type
(
abnf::tree-optionp
next-token)
.
rest-input
—
Type
(
abnf::tree-listp
rest-input)
.