• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Error-checking
        • Apt
        • Abnf
          • Defdefparse
          • Deftreeops
          • Defgrammar
          • Notation
            • Syntax-abstraction
            • Semantics
            • Abstract-syntax
            • Core-rules
              • Core-rule-names
              • Core-rule-definitions
              • Core-rules-validation
              • *core-rules*
            • Concrete-syntax
          • Grammar-parser
          • Meta-circular-validation
          • Parsing-primitives-defresult
          • Parsing-primitives-seq
          • Operations
          • Differences-with-paper
          • Examples
          • Grammar-printer
          • Parsing-tools
        • Fty-extensions
        • Isar
        • Kestrel-utilities
        • Prime-field-constraint-systems
        • Soft
        • Bv
        • Imp-language
        • Event-macros
        • Bitcoin
        • Ethereum
        • Yul
        • Zcash
        • ACL2-programming-language
        • Prime-fields
        • Java
        • C
        • Syntheto
        • Number-theory
        • Cryptography
        • Lists-light
        • File-io-light
        • Json
        • Built-ins
        • Solidity
        • Axe
        • Std-extensions
        • Htclient
        • Typed-lists-light
        • Arithmetic-light
      • X86isa
      • Execloader
      • Axe
    • Testing-utilities
    • Math
  • Notation
  • Concrete-syntax

Core-rules

Core rules of ABNF.

These rules are specified in [RFC:B]. They are a set of rules commonly used as part of the definition of the concrete syntax of languages in ABNF. In particular, they are used as part of the definition of the concrete syntax of ABNF itself in [RFC:4].

Since the concrete syntax of ABNF is specified, in [RFC:4], using ABNF concrete syntax, and since that definition of the concrete syntax of ABNF uses the core rules, we break the circularity by formalizing the core rules using the abstract syntax of ABNF.

Subtopics

Core-rule-names
Names of the core rules.
Core-rule-definitions
Definition of the core rules.
Core-rules-validation
Validation of the core rules.
*core-rules*
All the core rules.