		Search-engine friendly clone of the ACL2 documentation.

Concrete-syntax

Grammar

ABNF grammar of Yul.

We use our verified ABNF grammar parser to parse the ABNF grammar of Yul into a representation in ACL2.

Subtopics

Cst-literal-conc?
Cst-token-conc?
Cst-expression-conc?
Cst-list-list-conc-matchp$
Cst-lexeme-conc?
Cst-list-list-alt-matchp$
Cst-identifier-rest-conc?
Cst-list-rep-matchp$
Cst-list-elem-matchp$
Cst-comment-conc?
Abnf-tree-wrap-fn
Abnf-tree-with-root-p: Recognize terminated ABNF trees rooted at rulename, for the ABNF grammar of Yul.
Cst-nonzero-decimal-digit-conc-rep-elem
Cst-matchp$
Abnf-tree-wrap: Wrap an ABNF tree into a nest of ABNF trees with the given rule names as roots.
Cst-nonzero-decimal-digit-conc-rep
Cst-identifier-rest-conc2-rep-elem
Cst-identifier-rest-conc2-rep
Cst-identifier-rest-conc1-rep-elem
Cst-identifier-rest-conc1-rep
Cst-expression-conc3-rep-elem
Cst-expression-conc2-rep-elem
Cst-uppercase-letter-conc-rep-elem
Cst-uppercase-letter-conc-rep
Cst-switch-statement-conc
Cst-nonzero-decimal-digit-conc
Cst-lowercase-letter-conc-rep-elem
Cst-lowercase-letter-conc-rep
Cst-literal-conc5-rep-elem
Cst-literal-conc4-rep-elem
Cst-literal-conc3-rep-elem
Cst-literal-conc2-rep-elem
Cst-literal-conc1-rep-elem
Cst-lexeme-conc3-rep-elem
Cst-lexeme-conc2-rep-elem
Cst-lexeme-conc1-rep-elem
Cst-identifier-rest-conc2
Cst-identifier-rest-conc1
Cst-function-definition-conc
Cst-expression-conc3-rep
Cst-expression-conc2-rep
Cst-expression-conc1-rep-elem
Cst-expression-conc1-rep
Cst-end-of-line-comment-conc
Cst-decimal-digit-conc-rep-elem
Cst-comment-conc2-rep-elem
Cst-comment-conc1-rep-elem
Cst-uppercase-letter-conc
Cst-token-conc4-rep-elem
Cst-token-conc3-rep-elem
Cst-token-conc2-rep-elem
Cst-token-conc1-rep-elem
Cst-lowercase-letter-conc
Cst-literal-conc5-rep
Cst-literal-conc5
Cst-literal-conc4-rep
Cst-literal-conc4
Cst-literal-conc3-rep
Cst-literal-conc3
Cst-literal-conc2-rep
Cst-literal-conc2
Cst-literal-conc1-rep
Cst-literal-conc1
Cst-lexeme-conc3-rep
Cst-lexeme-conc2-rep
Cst-lexeme-conc1-rep
Cst-if-statement-conc
Cst-function-call-conc
Cst-for-statement-conc
Cst-expression-conc3
Cst-expression-conc2
Cst-expression-conc1
Cst-escape-sequence-conc
Cst-decimal-digit-conc-rep
Cst-decimal-digit-conc
Cst-comment-conc2-rep
Cst-comment-conc2
Cst-comment-conc1-rep
Cst-comment-conc1
Cst-block-comment-conc
Cst-whitespace-conc
Cst-token-conc4-rep
Cst-token-conc4
Cst-token-conc3-rep
Cst-token-conc3
Cst-token-conc2-rep
Cst-token-conc2
Cst-token-conc1-rep
Cst-token-conc1
Cst-squote-conc-rep-elem
Cst-squote-conc-rep
Cst-lexeme-conc3
Cst-lexeme-conc2
Cst-lexeme-conc1
Cst-identifier-conc
Cst-hex-string-conc
Cst-hex-number-conc
Cst-dquote-conc-rep-elem
Cst-dquote-conc-rep
*grammar*: The parsed ABNF grammar of Yul.
Cst-squote-conc
Cst-path-conc
Cst-lf-conc-rep-elem
Cst-lf-conc-rep
Cst-dquote-conc
Cst-cr-conc-rep-elem
Cst-cr-conc-rep
Cst-block-conc
Abnf-tree-list-with-root-p: Lift abnf-tree-with-root-p to lists
Cst-lf-conc
Cst-cr-conc
Cst-%xe-7f-nat
Cst-%xb-c-nat
Cst-%x61-7a-nat
Cst-%x5d-7e-nat
Cst-%x41-5a-nat
Cst-%x31-39-nat
Cst-%x30-7f-nat
Cst-%x30-39-nat
Cst-%x2b-7f-nat
Cst-%x2b-2e-nat
Cst-%x28-5b-nat
Cst-%x23-5b-nat
Cst-%x20-26-nat
Cst-%x20-21-nat
Cst-%x0-9-nat
Cst-%x0-29-nat