		Search-engine friendly clone of the ACL2 documentation.

Concrete-syntax

Grammar

ABNF grammar of Leo.

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

The grammar consists of three sub-grammars: the lexical grammar, the syntactic grammar, and the format string grammar. We put them together, in one ACL2 constant for the whole grammar.

Subtopics

Cst-statement-conc?
Cst-simple-character-escape-conc?
Cst-not-line-feed-or-carriage-return-conc?
Cst-token-conc?
Cst-program-item-conc?
Cst-string-literal-element-conc?
Cst-safe-ascii-conc?
Cst-postfix-expression-conc?
Cst-named-primitive-type-conc?
Cst-numeric-literal-conc?
Cst-atomic-literal-conc?
Cst-arithmetic-type-conc?
Abnf-tree-with-root-p: Recognize CSTs whose root is the given rule name, for the ABNF grammar of Leo.
Cst-console-call-conc?
Cst-whitespace-conc?
Cst-type-conc?
Cst-list-list-conc-matchp$
Cst-lexeme-conc?
Cst-primitive-type-conc?
Cst-operator-call-conc?
Cst-list-list-alt-matchp$
Cst-integer-literal-conc?
Cst-group-literal-conc?
Cst-not-line-feed-or-carriage-return-conc4-rep-elem
Cst-not-line-feed-or-carriage-return-conc3-rep-elem
Cst-not-line-feed-or-carriage-return-conc2-rep-elem
Cst-not-line-feed-or-carriage-return-conc1-rep-elem
Cst-integer-type-conc?
Cst-not-line-feed-or-carriage-return-conc4-rep
Cst-not-line-feed-or-carriage-return-conc3-rep
Cst-not-line-feed-or-carriage-return-conc2-rep
Cst-not-line-feed-or-carriage-return-conc1-rep
Cst-literal-conc?
Cst-list-rep-matchp$
Cst-list-elem-matchp$
Cst-letter-conc?
Cst-comment-conc?
Cst-character-conc?
Cst-not-line-feed-or-carriage-return-conc4
Cst-not-line-feed-or-carriage-return-conc3
Cst-not-line-feed-or-carriage-return-conc2
Cst-not-line-feed-or-carriage-return-conc1
Abnf-tree-wrap-fn
Abnf-tree-wrap: Wrap a CST into a nest of CSTs with the given rule names as roots (in the order given) and each with a single subtree, ending with the original tree.
Cst-string-literal-element-conc4-rep-elem
Cst-string-literal-element-conc3-rep-elem
Cst-string-literal-element-conc2-rep-elem
Cst-string-literal-element-conc1-rep-elem
Cst-string-literal-element-conc1-rep
Cst-simple-character-escape-conc7-rep-elem
Cst-simple-character-escape-conc7-rep
Cst-simple-character-escape-conc6-rep-elem
Cst-simple-character-escape-conc6-rep
Cst-simple-character-escape-conc5-rep-elem
Cst-simple-character-escape-conc5-rep
Cst-simple-character-escape-conc4-rep-elem
Cst-simple-character-escape-conc4-rep
Cst-simple-character-escape-conc3-rep-elem
Cst-simple-character-escape-conc3-rep
Cst-simple-character-escape-conc2-rep-elem
Cst-simple-character-escape-conc2-rep
Cst-simple-character-escape-conc1-rep-elem
Cst-simple-character-escape-conc1-rep
Cst-named-primitive-type-conc4-rep-elem
Cst-named-primitive-type-conc3-rep-elem
Cst-named-primitive-type-conc2-rep-elem
Cst-named-primitive-type-conc1-rep-elem
Cst-variable-or-free-constant-conc-rep-elem
Cst-variable-or-free-constant-conc-rep
Cst-tuple-component-expression-conc
Cst-struct-component-expression-conc
Cst-struct-component-declarations-conc
Cst-struct-component-declaration-conc
Cst-string-literal-element-conc4-rep
Cst-string-literal-element-conc4
Cst-string-literal-element-conc3-rep
Cst-string-literal-element-conc3
Cst-string-literal-element-conc2-rep
Cst-string-literal-element-conc2
Cst-string-literal-element-conc1
Cst-simple-character-escape-conc7
Cst-simple-character-escape-conc6
Cst-simple-character-escape-conc5
Cst-simple-character-escape-conc4
Cst-simple-character-escape-conc3
Cst-simple-character-escape-conc2
Cst-simple-character-escape-conc1
Cst-postfix-expression-conc4-rep-elem
Cst-postfix-expression-conc4-rep
Cst-postfix-expression-conc3-rep-elem
Cst-postfix-expression-conc3-rep
Cst-postfix-expression-conc2-rep-elem
Cst-postfix-expression-conc2-rep
Cst-postfix-expression-conc1-rep-elem
Cst-postfix-expression-conc1-rep
Cst-numeric-literal-conc3-rep-elem
Cst-named-primitive-type-conc4-rep
Cst-named-primitive-type-conc3-rep
Cst-named-primitive-type-conc2-rep
Cst-named-primitive-type-conc1-rep
Cst-matchp$
Cst-carriage-return-escape-conc-rep-elem
Cst-whitespace-conc3-rep-elem
Cst-whitespace-conc2-rep-elem
Cst-whitespace-conc1-rep-elem
Cst-variable-or-free-constant-conc
Cst-unicode-character-escape-conc
Cst-transition-declaration-conc
Cst-safe-ascii-conc5-rep-elem
Cst-safe-ascii-conc4-rep-elem
Cst-safe-ascii-conc3-rep-elem
Cst-safe-ascii-conc2-rep-elem
Cst-safe-ascii-conc1-rep-elem
Cst-program-item-conc5-rep-elem
Cst-program-item-conc4-rep-elem
Cst-program-item-conc3-rep-elem
Cst-program-item-conc2-rep-elem
Cst-program-item-conc1-rep-elem
Cst-primitive-type-conc2-rep-elem
Cst-primitive-type-conc2-rep
Cst-primitive-type-conc1-rep-elem
Cst-primitive-type-conc1-rep
Cst-postfix-expression-conc4
Cst-postfix-expression-conc3
Cst-postfix-expression-conc2
Cst-postfix-expression-conc1
Cst-output-expression-conc-rep-elem
Cst-operator-call-conc2-rep-elem
Cst-operator-call-conc2-rep
Cst-operator-call-conc1-rep-elem
Cst-operator-call-conc1-rep
Cst-numeric-literal-conc4-rep-elem
Cst-numeric-literal-conc4-rep
Cst-numeric-literal-conc3-rep
Cst-numeric-literal-conc2-rep-elem
Cst-numeric-literal-conc2-rep
Cst-numeric-literal-conc1-rep-elem
Cst-numeric-literal-conc1-rep
Cst-null-character-escape-conc-rep-elem
Cst-null-character-escape-conc-rep
Cst-named-primitive-type-conc4
Cst-named-primitive-type-conc3
Cst-named-primitive-type-conc2
Cst-named-primitive-type-conc1
Cst-integer-type-conc2-rep-elem
Cst-integer-type-conc1-rep-elem
Cst-integer-literal-conc2-rep-elem
Cst-integer-literal-conc2-rep
Cst-integer-literal-conc1-rep-elem
Cst-integer-literal-conc1-rep
Cst-horizontal-tab-escape-conc-rep-elem
Cst-horizontal-tab-escape-conc-rep
Cst-group-literal-conc2-rep-elem
Cst-group-literal-conc2-rep
Cst-group-literal-conc1-rep-elem
Cst-group-literal-conc1-rep
Cst-console-call-conc3-rep-elem
Cst-console-call-conc2-rep-elem
Cst-console-call-conc1-rep-elem
Cst-carriage-return-escape-conc-rep
Cst-binary-expression-conc-rep-elem
Cst-atomic-literal-conc4-rep-elem
Cst-atomic-literal-conc4-rep
Cst-atomic-literal-conc3-rep-elem
Cst-atomic-literal-conc3-rep
Cst-atomic-literal-conc2-rep-elem
Cst-atomic-literal-conc2-rep
Cst-atomic-literal-conc1-rep-elem
Cst-atomic-literal-conc1-rep
Cst-ascii-character-escape-conc
Cst-arithmetic-type-conc4-rep-elem
Cst-arithmetic-type-conc4-rep
Cst-arithmetic-type-conc3-rep-elem
Cst-arithmetic-type-conc3-rep
Cst-arithmetic-type-conc2-rep-elem
Cst-arithmetic-type-conc2-rep
Cst-arithmetic-type-conc1-rep-elem
Cst-arithmetic-type-conc1-rep
Cst-whitespace-conc3-rep
Cst-whitespace-conc2-rep
Cst-whitespace-conc1-rep
Cst-visible-ascii-conc-rep-elem
Cst-variable-declaration-conc
Cst-uppercase-letter-conc-rep-elem
Cst-uppercase-letter-conc-rep
Cst-unary-operator-call-conc
Cst-tuple-expression-conc
Cst-struct-expression-conc
Cst-struct-declaration-conc
Cst-static-function-call-conc
Cst-statement-conc9-rep-elem
Cst-statement-conc9-rep
Cst-statement-conc8-rep-elem
Cst-statement-conc8-rep
Cst-statement-conc7-rep-elem
Cst-statement-conc7-rep
Cst-statement-conc6-rep-elem
Cst-statement-conc6-rep
Cst-statement-conc5-rep-elem
Cst-statement-conc5-rep
Cst-statement-conc4-rep-elem
Cst-statement-conc4-rep
Cst-statement-conc3-rep-elem
Cst-statement-conc3-rep
Cst-statement-conc2-rep-elem
Cst-statement-conc2-rep
Cst-statement-conc11-rep-elem
Cst-statement-conc11-rep
Cst-statement-conc10-rep-elem
Cst-statement-conc10-rep
Cst-statement-conc1-rep-elem
Cst-statement-conc1-rep
Cst-single-quote-escape-conc
Cst-single-quote-conc-rep-elem
Cst-safe-ascii-conc5-rep
Cst-safe-ascii-conc4-rep
Cst-safe-ascii-conc3-rep
Cst-safe-ascii-conc2-rep
Cst-safe-ascii-conc1-rep
Cst-record-declaration-conc
Cst-program-item-conc5-rep
Cst-program-item-conc5
Cst-program-item-conc4-rep
Cst-program-item-conc4
Cst-program-item-conc3-rep
Cst-program-item-conc3
Cst-program-item-conc2-rep
Cst-program-item-conc2
Cst-program-item-conc1-rep
Cst-program-item-conc1
Cst-program-declaration-conc
Cst-product-group-literal-conc
Cst-primitive-type-conc2
Cst-primitive-type-conc1
Cst-output-expression-conc-rep
Cst-operator-call-conc2
Cst-operator-call-conc1
Cst-numeric-literal-conc4
Cst-numeric-literal-conc3
Cst-numeric-literal-conc2
Cst-numeric-literal-conc1
Cst-null-character-escape-conc
Cst-mapping-declaration-conc
Cst-lowercase-letter-conc-rep-elem
Cst-lowercase-letter-conc-rep
Cst-literal-conc2-rep-elem
Cst-literal-conc1-rep-elem
Cst-line-feed-escape-conc-rep-elem
Cst-line-feed-escape-conc-rep
Cst-lexeme-conc3-rep-elem
Cst-lexeme-conc2-rep-elem
Cst-lexeme-conc1-rep-elem
Cst-letter-conc2-rep-elem
Cst-letter-conc1-rep-elem
Cst-integer-type-conc2-rep
Cst-integer-type-conc2
Cst-integer-type-conc1-rep
Cst-integer-type-conc1
Cst-integer-literal-conc2
Cst-integer-literal-conc1
Cst-input-expression-conc-rep-elem
Cst-input-expression-conc-rep
Cst-increment-statement-conc
Cst-import-declaration-conc
Cst-horizontal-tab-escape-conc
Cst-horizontal-tab-conc-rep-elem
Cst-group-literal-conc2
Cst-group-literal-conc1
Cst-function-parameters-conc
Cst-function-parameter-conc
Cst-function-declaration-conc
Cst-function-arguments-conc
Cst-finalize-statement-conc
Cst-double-quote-escape-conc
Cst-double-quote-conc-rep-elem
Cst-decrement-statement-conc
Cst-decimal-digit-conc-rep-elem
Cst-constant-declaration-conc
Cst-console-statement-conc
Cst-console-call-conc3-rep
Cst-console-call-conc3
Cst-console-call-conc2-rep
Cst-console-call-conc2
Cst-console-call-conc1-rep
Cst-console-call-conc1
Cst-comment-conc2-rep-elem
Cst-comment-conc1-rep-elem
Cst-character-conc2-rep-elem
Cst-character-conc2-rep
Cst-character-conc1-rep-elem
Cst-character-conc1-rep
Cst-carriage-return-escape-conc
Cst-carriage-return-conc-rep-elem
Cst-carriage-return-conc-rep
Cst-boolean-type-conc-rep-elem
Cst-binary-operator-call-conc
Cst-binary-expression-conc-rep
Cst-binary-expression-conc
Cst-backslash-escape-conc-rep-elem
Cst-backslash-escape-conc-rep
Cst-atomic-literal-conc4
Cst-atomic-literal-conc3
Cst-atomic-literal-conc2
Cst-atomic-literal-conc1
Cst-associated-constant-conc
Cst-assignment-statement-conc
Cst-assert-not-equal-call-conc
Cst-assert-equal-call-conc
Cst-arithmetic-type-conc4
Cst-arithmetic-type-conc3
Cst-arithmetic-type-conc2
Cst-arithmetic-type-conc1
Cst-affine-group-literal-conc
Cst-address-type-conc-rep-elem
Cst-whitespace-conc3
Cst-whitespace-conc2
Cst-whitespace-conc1
Cst-visible-ascii-conc-rep
Cst-visible-ascii-conc
Cst-uppercase-letter-conc
Cst-unsigned-literal-conc
Cst-unit-expression-conc
Cst-type-conc3-rep-elem
Cst-type-conc2-rep-elem
Cst-type-conc1-rep-elem
Cst-token-conc6-rep-elem
Cst-token-conc5-rep-elem
Cst-token-conc4-rep-elem
Cst-token-conc3-rep-elem
Cst-token-conc2-rep-elem
Cst-token-conc1-rep-elem
Cst-string-type-conc-rep-elem
Cst-string-type-conc-rep
Cst-string-literal-conc
Cst-statement-conc9
Cst-statement-conc8
Cst-statement-conc7
Cst-statement-conc6
Cst-statement-conc5
Cst-statement-conc4
Cst-statement-conc3
Cst-statement-conc2
Cst-statement-conc11
Cst-statement-conc10
Cst-statement-conc1
Cst-single-quote-conc-rep
Cst-signed-literal-conc
Cst-scalar-type-conc-rep-elem
Cst-scalar-type-conc-rep
Cst-scalar-literal-conc
Cst-safe-ascii-conc5
Cst-safe-ascii-conc4
Cst-safe-ascii-conc3
Cst-safe-ascii-conc2
Cst-safe-ascii-conc1
Cst-return-statement-conc
Cst-output-section-conc
Cst-output-file-conc-rep-elem
Cst-output-file-conc-rep
Cst-output-expression-conc
Cst-octal-digit-conc-rep-elem
Cst-octal-digit-conc-rep
Cst-lowercase-letter-conc
Cst-loop-statement-conc
Cst-literal-conc2-rep
Cst-literal-conc2
Cst-literal-conc1-rep
Cst-literal-conc1
Cst-line-feed-escape-conc
Cst-line-feed-conc-rep-elem
Cst-line-comment-conc
Cst-lexeme-conc3-rep
Cst-lexeme-conc2-rep
Cst-lexeme-conc1-rep
Cst-letter-conc2-rep
Cst-letter-conc1-rep
Cst-input-type-conc-rep-elem
Cst-input-section-conc
Cst-input-expression-conc
Cst-horizontal-tab-conc-rep
Cst-horizontal-tab-conc
Cst-group-type-conc-rep-elem
Cst-field-type-conc-rep-elem
Cst-field-literal-conc
Cst-expression-conc-rep-elem
Cst-expression-conc-rep
Cst-double-quote-conc-rep
Cst-decimal-digit-conc-rep
Cst-decimal-digit-conc
Cst-comment-conc2-rep
Cst-comment-conc2
Cst-comment-conc1-rep
Cst-comment-conc1
Cst-character-conc2
Cst-character-conc1
Cst-carriage-return-conc
Cst-boolean-type-conc-rep
Cst-block-comment-conc
Cst-backslash-escape-conc
Cst-address-type-conc-rep
Cst-address-literal-conc
*grammar*: The parsed ABNF grammar of Leo.
Cst-unit-type-conc
Cst-type-conc3-rep
Cst-type-conc3
Cst-type-conc2-rep
Cst-type-conc2
Cst-type-conc1-rep
Cst-type-conc1
Cst-tuple-type-conc
Cst-token-conc6-rep
Cst-token-conc6
Cst-token-conc5-rep
Cst-token-conc5
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-string-type-conc
Cst-space-conc-rep-elem
Cst-single-quote-conc
Cst-scalar-type-conc
Cst-program-id-conc
Cst-output-title-conc
Cst-output-item-conc
Cst-output-file-conc
Cst-octal-digit-conc
Cst-locator-conc
Cst-line-feed-conc-rep
Cst-line-feed-conc
Cst-lexeme-conc3
Cst-lexeme-conc2
Cst-lexeme-conc1
Cst-letter-conc2
Cst-letter-conc1
Cst-input-type-conc-rep
Cst-input-type-conc
Cst-input-title-conc
Cst-input-item-conc
Cst-input-file-conc
Cst-identifier-conc
Cst-group-type-conc-rep
Cst-group-type-conc
Cst-finalizer-conc
Cst-field-type-conc-rep
Cst-field-type-conc
Cst-expression-conc
Cst-double-quote-conc
Cst-boolean-type-conc
Cst-assert-call-conc
Cst-annotation-conc
Cst-address-type-conc
Cst-space-conc-rep
Cst-space-conc
Cst-numeral-conc
Cst-file-conc
Cst-branch-conc
Cst-block-conc
Abnf-tree-list-with-root-p: Lift abnf-tree-with-root-p to lists.
Cst-%xe000-10ffff-nat
Cst-%x206a-d7ff-nat
Cst-%x202f-2065-nat
Cst-%x80-2029-nat
Cst-%x61-7a-nat
Cst-%x5d-7e-nat
Cst-%x41-5a-nat
Cst-%x30-7e-nat
Cst-%x30-39-nat
Cst-%x30-37-nat
Cst-%x2b-7e-nat
Cst-%x2b-2e-nat
Cst-%x23-5b-nat
Cst-%x21-7e-nat
Cst-%x20-29-nat
Cst-%x20-21-nat