• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
        • Error-checking
        • Fty-extensions
        • Isar
        • Kestrel-utilities
        • Set
        • Soft
        • C
        • Bv
        • Imp-language
        • Event-macros
        • Java
        • Bitcoin
        • Ethereum
        • Yul
        • Zcash
        • ACL2-programming-language
        • Prime-fields
        • Json
          • Parser-output-to-values
          • Values
          • Syntax
            • Grammar
              • Cst-value-conc?
              • *all-grammar-rules*
              • Cst-list-list-conc-matchp$
              • Cst-list-list-alt-matchp$
              • Cst-list-rep-matchp$
              • Cst-list-elem-matchp$
              • Cst-matchp$
              • Cst-quotation-mark-conc-rep-elem
              • Cst-decimal-point-conc-rep-elem
              • Cst-value-separator-conc
              • Cst-value-conc7-rep-elem
              • Cst-value-conc6-rep-elem
              • Cst-value-conc5-rep-elem
              • Cst-value-conc4-rep-elem
              • Cst-value-conc3-rep-elem
              • Cst-value-conc2-rep-elem
              • Cst-value-conc1-rep-elem
              • Cst-quotation-mark-conc-rep
              • Cst-quotation-mark-conc
              • Cst-name-separator-conc
              • Cst-digit1-9-conc-rep-elem
              • Cst-decimal-point-conc-rep
              • Cst-decimal-point-conc
              • Cst-zero-conc-rep-elem
              • Cst-value-conc7-rep
              • Cst-value-conc7
              • Cst-value-conc6-rep
              • Cst-value-conc6
              • Cst-value-conc5-rep
              • Cst-value-conc5
              • Cst-value-conc4-rep
              • Cst-value-conc4
              • Cst-value-conc3-rep
              • Cst-value-conc3
              • Cst-value-conc2-rep
              • Cst-value-conc2
              • Cst-value-conc1-rep
              • Cst-value-conc1
              • Cst-true-conc-rep-elem
              • Cst-string-conc
              • Cst-plus-conc-rep-elem
              • Cst-null-conc-rep-elem
              • Cst-minus-conc-rep-elem
              • Cst-member-conc
              • Cst-json-text-conc
              • Cst-false-conc-rep-elem
              • Cst-escape-conc-rep-elem
              • Cst-escape-conc-rep
              • Cst-end-object-conc
              • Cst-end-array-conc
              • Cst-digit1-9-conc-rep
              • Cst-digit1-9-conc
              • Cst-digit-conc-rep-elem
              • Cst-begin-object-conc
              • Cst-begin-array-conc
              • *grammar-rules*
              • Cst-zero-conc-rep
              • Cst-zero-conc
              • Cst-ws-conc
              • Cst-true-conc-rep
              • Cst-true-conc
              • Cst-plus-conc-rep
              • Cst-plus-conc
              • Cst-object-conc
              • Cst-number-conc
              • Cst-null-conc-rep
              • Cst-null-conc
              • Cst-minus-conc-rep
              • Cst-minus-conc
              • Cst-frac-conc
              • Cst-false-conc-rep
              • Cst-false-conc
              • Cst-exp-conc
              • Cst-escape-conc
              • Cst-digit-conc-rep
              • Cst-digit-conc
              • Cst-array-conc
              • Cst-%x5d-10ffff-nat
              • Cst-%x31-39-nat
              • Cst-%x30-39-nat
              • Cst-%x23-5b-nat
              • Cst-%x20-21-nat
          • Patbind-pattern
          • Operations
        • Syntheto
        • File-io-light
        • Cryptography
        • Number-theory
        • Lists-light
        • Axe
        • Builtins
        • Solidity
        • Helpers
        • Htclient
        • Typed-lists-light
        • Arithmetic-light
      • X86isa
      • Axe
      • Execloader
    • Math
    • Testing-utilities
  • Syntax

Grammar

The ABNF grammar of JSON.

Subtopics

Cst-value-conc?
*all-grammar-rules*
All the JSON grammar rules, including the referenced ABNF core rules.
Cst-list-list-conc-matchp$
Cst-list-list-alt-matchp$
Cst-list-rep-matchp$
Cst-list-elem-matchp$
Cst-matchp$
Cst-quotation-mark-conc-rep-elem
Cst-decimal-point-conc-rep-elem
Cst-value-separator-conc
Cst-value-conc7-rep-elem
Cst-value-conc6-rep-elem
Cst-value-conc5-rep-elem
Cst-value-conc4-rep-elem
Cst-value-conc3-rep-elem
Cst-value-conc2-rep-elem
Cst-value-conc1-rep-elem
Cst-quotation-mark-conc-rep
Cst-quotation-mark-conc
Cst-name-separator-conc
Cst-digit1-9-conc-rep-elem
Cst-decimal-point-conc-rep
Cst-decimal-point-conc
Cst-zero-conc-rep-elem
Cst-value-conc7-rep
Cst-value-conc7
Cst-value-conc6-rep
Cst-value-conc6
Cst-value-conc5-rep
Cst-value-conc5
Cst-value-conc4-rep
Cst-value-conc4
Cst-value-conc3-rep
Cst-value-conc3
Cst-value-conc2-rep
Cst-value-conc2
Cst-value-conc1-rep
Cst-value-conc1
Cst-true-conc-rep-elem
Cst-string-conc
Cst-plus-conc-rep-elem
Cst-null-conc-rep-elem
Cst-minus-conc-rep-elem
Cst-member-conc
Cst-json-text-conc
Cst-false-conc-rep-elem
Cst-escape-conc-rep-elem
Cst-escape-conc-rep
Cst-end-object-conc
Cst-end-array-conc
Cst-digit1-9-conc-rep
Cst-digit1-9-conc
Cst-digit-conc-rep-elem
Cst-begin-object-conc
Cst-begin-array-conc
*grammar-rules*
The JSON grammar rules from RFC 8259.
Cst-zero-conc-rep
Cst-zero-conc
Cst-ws-conc
Cst-true-conc-rep
Cst-true-conc
Cst-plus-conc-rep
Cst-plus-conc
Cst-object-conc
Cst-number-conc
Cst-null-conc-rep
Cst-null-conc
Cst-minus-conc-rep
Cst-minus-conc
Cst-frac-conc
Cst-false-conc-rep
Cst-false-conc
Cst-exp-conc
Cst-escape-conc
Cst-digit-conc-rep
Cst-digit-conc
Cst-array-conc
Cst-%x5d-10ffff-nat
Cst-%x31-39-nat
Cst-%x30-39-nat
Cst-%x23-5b-nat
Cst-%x20-21-nat