• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
        • Deftreeops
        • Defdefparse
        • Defgrammar
        • Tree-utilities
        • Notation
          • Syntax-abstraction
          • Semantics
            • Tree-terminatedp
            • Tree->string
            • String-has-finite-parse-trees-p
            • Parse-trees-of-string-p
            • Tree-match-element-p
            • Parse-treep
            • Symbol
              • Symbol-fix
              • Symbol-equiv
              • Symbol-nonterminal
              • Symbol-terminal
              • Symbolp
              • Symbol-kind
              • Symbolp-when-rulenamep
              • Symbolp-alt-def
              • Disjoint-nat/rulename
              • Symbolp-when-natp
            • String-unambiguousp
            • Tree-match-num-val-p
            • Nat-match-insensitive-char-p
            • Nats-match-insensitive-chars-p
            • Tree-option
            • String-parsablep
            • Lookup-rulename
            • Nats-match-sensitive-chars-p
            • Numrep-match-repeat-range-p
            • Tree-match-char-val-p
            • Tree-list-match-repetition-p
            • String-ambiguousp
            • Parse
            • Tree-match-prose-val-p
            • Nat-match-sensitive-char-p
            • Theorems-about-terminated-trees-matching-elements
            • Tree-option-result
            • Tree-list-result
            • Tree-list-list-result
            • Tree-result
            • Tree-list-list-match-concatenation-p
            • Languagep
            • Terminal-string-for-rules-p
            • Tree-list-list-match-alternation-p
            • Tree-list-match-element-p
            • Parse!
            • String
            • Tree-set
            • Trees
          • Abstract-syntax
          • Core-rules
          • Concrete-syntax
        • Grammar-parser
        • Meta-circular-validation
        • Parsing-primitives-defresult
        • Parsing-primitives-seq
        • Operations
        • Examples
        • Differences-with-paper
        • Constructor-utilities
        • Grammar-printer
        • Parsing-tools
      • Vwsim
      • Isar
      • Wp-gen
      • Dimacs-reader
      • Pfcs
      • Legacy-defrstobj
      • Proof-checker-array
      • Soft
      • C
      • Farray
      • Rp-rewriter
      • Instant-runoff-voting
      • Imp-language
      • Sidekick
      • Leftist-trees
      • Java
      • Taspi
      • Bitcoin
      • Riscv
      • Des
      • Ethereum
      • X86isa
      • Sha-2
      • Yul
      • Zcash
      • Proof-checker-itp13
      • Regex
      • ACL2-programming-language
      • Json
      • Jfkr
      • Equational
      • Cryptography
      • Poseidon
      • Where-do-i-place-my-book
      • Axe
      • Bigmems
      • Builtins
      • Execloader
      • Aleo
      • Solidity
      • Paco
      • Concurrent-programs
      • Bls12-377-curves
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Semantics

Symbol

Symbols.

This is a sum-of-products (i.e., union) type, introduced by fty::defflexsum.

Members
:terminal → symbol-terminal
:nonterminal → symbol-nonterminal

As explained in [RFC:2.3], the terminal values of ABNF are natural numbers.

Rule names are the nonterminal symbols of ABNF.

In analogy with the typical notion of formal grammar in textbooks, an ABNF symbol is a terminal or a nonterminal, i.e. a natural number or a rule name.

Since natural numbers and rule names are disjoint, we put them together without tags.

Subtopics

Symbol-fix
Fixing function for symbol structures.
Symbol-equiv
Basic equivalence relation for symbol structures.
Symbol-nonterminal
Symbol-terminal
Symbolp
Recognizer for symbol structures.
Symbol-kind
Get the kind (tag) of a symbol structure.
Symbolp-when-rulenamep
Symbolp-alt-def
Disjoint-nat/rulename
Symbolp-when-natp