		Search-engine friendly clone of the ACL2 documentation.

Concrete-syntax

Grammar

ABNF grammar of Aleo instructions.

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

Subtopics

Cst-safe-ascii-conc?
Cst-arithmetic-literal-conc?
Cst-arithmetic-type-conc?
Cst-not-lf-or-cr-conc?
Cst-literal-type-conc?
Cst-plain-ws-conc?
Cst-literal-conc?
Cst-string-element-conc?
Cst-command-conc?
Cst-list-list-conc-matchp$
Cst-plaintext-type-conc?
Cst-list-list-alt-matchp$
Cst-integer-literal-conc?
Cst-integer-type-conc?
Cst-list-rep-matchp$
Cst-list-elem-matchp$
Cst-letter-conc?
Cst-comment-conc?
Cst-character-conc?
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-matchp$
Cst-arithmetic-literal-conc4-rep-elem
Cst-arithmetic-literal-conc4-rep
Cst-arithmetic-literal-conc3-rep-elem
Cst-arithmetic-literal-conc3-rep
Cst-arithmetic-literal-conc2-rep-elem
Cst-arithmetic-literal-conc2-rep
Cst-arithmetic-literal-conc1-rep-elem
Cst-arithmetic-literal-conc1-rep
Cst-string-element-conc3-rep-elem
Cst-string-element-conc3-rep
Cst-string-element-conc2-rep-elem
Cst-string-element-conc2-rep
Cst-string-element-conc1-rep-elem
Cst-string-element-conc1-rep
Cst-safe-ascii-conc5-rep-elem
Cst-plaintext-type-conc2-rep-elem
Cst-plaintext-type-conc2-rep
Cst-plaintext-type-conc1-rep-elem
Cst-plaintext-type-conc1-rep
Cst-not-lf-or-cr-conc4-rep-elem
Cst-not-lf-or-cr-conc3-rep-elem
Cst-not-lf-or-cr-conc2-rep-elem
Cst-not-lf-or-cr-conc1-rep-elem
Cst-literal-type-conc4-rep-elem
Cst-literal-type-conc3-rep-elem
Cst-literal-type-conc2-rep-elem
Cst-literal-type-conc1-rep-elem
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-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-arithmetic-literal-conc4
Cst-arithmetic-literal-conc3
Cst-arithmetic-literal-conc2
Cst-arithmetic-literal-conc1
Cst-visible-ascii-conc-rep-elem
Cst-uppercase-letter-conc-rep-elem
Cst-uppercase-letter-conc-rep
Cst-unsigned-literal-conc
Cst-transition-output-conc
Cst-string-element-conc3
Cst-string-element-conc2
Cst-string-element-conc1
Cst-safe-ascii-conc5-rep
Cst-safe-ascii-conc4-rep-elem
Cst-safe-ascii-conc4-rep
Cst-safe-ascii-conc3-rep-elem
Cst-safe-ascii-conc3-rep
Cst-safe-ascii-conc2-rep-elem
Cst-safe-ascii-conc2-rep
Cst-safe-ascii-conc1-rep-elem
Cst-safe-ascii-conc1-rep
Cst-plaintext-type-conc2
Cst-plaintext-type-conc1
Cst-plain-ws-conc4-rep-elem
Cst-plain-ws-conc3-rep-elem
Cst-plain-ws-conc2-rep-elem
Cst-plain-ws-conc1-rep-elem
Cst-not-lf-or-cr-conc4-rep
Cst-not-lf-or-cr-conc4
Cst-not-lf-or-cr-conc3-rep
Cst-not-lf-or-cr-conc3
Cst-not-lf-or-cr-conc2-rep
Cst-not-lf-or-cr-conc2
Cst-not-lf-or-cr-conc1-rep
Cst-not-lf-or-cr-conc1
Cst-lowercase-letter-conc-rep-elem
Cst-lowercase-letter-conc-rep
Cst-literal-type-conc4-rep
Cst-literal-type-conc4
Cst-literal-type-conc3-rep
Cst-literal-type-conc3
Cst-literal-type-conc2-rep
Cst-literal-type-conc2
Cst-literal-type-conc1-rep
Cst-literal-type-conc1
Cst-literal-conc4-rep-elem
Cst-literal-conc3-rep-elem
Cst-literal-conc2-rep-elem
Cst-literal-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-finalize-command-conc
Cst-comment-conc2-rep-elem
Cst-comment-conc1-rep-elem
Cst-command-conc3-rep-elem
Cst-command-conc2-rep-elem
Cst-command-conc1-rep-elem
Cst-character-conc2-rep-elem
Cst-character-conc2-rep
Cst-character-conc1-rep-elem
Cst-character-conc1-rep
Cst-boolean-type-conc-rep-elem
Cst-arithmetic-type-conc4
Cst-arithmetic-type-conc3
Cst-arithmetic-type-conc2
Cst-arithmetic-type-conc1
Cst-address-type-conc-rep-elem
Cst-visible-ascii-conc-rep
Cst-visible-ascii-conc
Cst-uppercase-letter-conc
Cst-transition-input-conc
Cst-ternary-op-conc-rep-elem
Cst-string-type-conc-rep-elem
Cst-string-type-conc-rep
Cst-string-literal-conc
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-register-access-conc
Cst-plain-ws-conc4-rep
Cst-plain-ws-conc4
Cst-plain-ws-conc3-rep
Cst-plain-ws-conc3
Cst-plain-ws-conc2-rep
Cst-plain-ws-conc2
Cst-plain-ws-conc1-rep
Cst-plain-ws-conc1
Cst-mapping-value-conc
Cst-lowercase-letter-conc
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-line-comment-conc
Cst-letter-conc2-rep
Cst-letter-conc1-rep
Cst-instruction-conc
Cst-group-type-conc-rep-elem
Cst-group-literal-conc
Cst-function-output-conc
Cst-function-input-conc
Cst-finalize-output-conc
Cst-finalize-input-conc
Cst-field-type-conc-rep-elem
Cst-field-literal-conc
Cst-escaped-char-conc
Cst-comment-conc2-rep
Cst-comment-conc2
Cst-comment-conc1-rep
Cst-comment-conc1
Cst-command-conc3-rep
Cst-command-conc3
Cst-command-conc2-rep
Cst-command-conc2
Cst-command-conc1-rep
Cst-command-conc1
Cst-character-conc2
Cst-character-conc1
Cst-boolean-type-conc-rep
Cst-block-comment-conc
Cst-address-type-conc-rep
Cst-address-literal-conc
Cst-transition-conc
Cst-ternary-op-conc-rep
Cst-ternary-op-conc
Cst-ternary-conc
Cst-struct-conc
Cst-string-type-conc
Cst-scalar-type-conc
Cst-register-conc
Cst-record-conc
Cst-program-id-conc
Cst-program-conc
Cst-mapping-key-conc
Cst-mapping-conc
Cst-locator-conc
Cst-letter-conc2
Cst-letter-conc1
Cst-increment-conc
Cst-identifier-conc
Cst-group-type-conc-rep
Cst-group-type-conc
Cst-function-conc
Cst-finalize-conc
Cst-field-type-conc-rep
Cst-field-type-conc
Cst-escaped-ws-conc
Cst-escaped-lf-conc
Cst-entry-type-conc
Cst-digit-conc-rep-elem
Cst-decrement-conc
Cst-boolean-type-conc
Cst-binary-conc
Cst-address-type-conc
*grammar*: The parsed ABNF grammar of Aleo instructions.
Cst-ws-conc
Cst-unary-conc
Cst-tuple-conc
Cst-sp-conc-rep-elem
Cst-sp-conc-rep
Cst-lf-conc-rep-elem
Cst-lf-conc-rep
Cst-is-conc
Cst-import-conc
Cst-ht-conc-rep-elem
Cst-ht-conc-rep
Cst-hash-conc
Cst-entry-conc
Cst-dq-conc-rep-elem
Cst-dq-conc-rep
Cst-digit-conc-rep
Cst-digit-conc
Cst-cws-conc
Cst-cr-conc-rep-elem
Cst-cr-conc-rep
Cst-commit-conc
Cst-cast-conc
Cst-call-conc
Cst-assert-conc
Cst-sp-conc
Cst-lf-conc
Cst-ht-conc
Cst-dq-conc
Cst-cr-conc
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-%x2b-7e-nat
Cst-%x2b-2e-nat
Cst-%x23-5b-nat
Cst-%x21-7e-nat
Cst-%x20-29-nat
Cst-%x20-21-nat