• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
        • Deftreeops
        • Defdefparse
        • Defgrammar
        • Tree-utilities
        • Notation
        • Grammar-parser
        • Meta-circular-validation
        • Parsing-primitives-defresult
        • Parsing-primitives-seq
        • Operations
        • Examples
          • Pdf-example
          • Smtp-example
          • Imap-example
          • Http-example
          • Uri-example
          • Imf-example
            • Imf-cst-received-token-conc?
            • Imf-cst-local-part-conc?
            • Imf-cst-id-right-conc?
            • Imf-cst-group-list-conc?
            • Imf-cst-domain-conc?
            • Imf-cst-ccontent-conc?
            • *all-imf-grammar-rules*
            • Imf-cst-list-list-conc-matchp$
            • Imf-cst-obs-dtext-conc?
            • Imf-cst-list-list-alt-matchp$
            • Imf-cst-qcontent-conc?
            • Imf-cst-mailbox-conc?
            • Imf-cst-id-left-conc?
            • Imf-cst-address-conc?
            • Imf-cst-wsp-conc?
            • Imf-cst-word-conc?
            • Imf-cst-list-rep-matchp$
            • Imf-cst-list-elem-matchp$
            • Imf-cst-received-token-conc4-rep-elem
            • Imf-cst-received-token-conc3-rep-elem
            • Imf-cst-received-token-conc2-rep-elem
            • Imf-cst-received-token-conc1-rep-elem
            • Imf-cst-received-token-conc4-rep
            • Imf-cst-received-token-conc3-rep
            • Imf-cst-received-token-conc2-rep
            • Imf-cst-received-token-conc1-rep
            • Imf-cst-matchp$
            • Imf-cst-local-part-conc3-rep-elem
            • Imf-cst-local-part-conc2-rep-elem
            • Imf-cst-local-part-conc1-rep-elem
            • Imf-cst-group-list-conc3-rep-elem
            • Imf-cst-group-list-conc2-rep-elem
            • Imf-cst-group-list-conc1-rep-elem
            • Imf-cst-received-token-conc4
            • Imf-cst-received-token-conc3
            • Imf-cst-received-token-conc2
            • Imf-cst-received-token-conc1
            • Imf-cst-qcontent-conc2-rep-elem
            • Imf-cst-qcontent-conc2-rep
            • Imf-cst-qcontent-conc1-rep-elem
            • Imf-cst-qcontent-conc1-rep
            • Imf-cst-obs-resent-rply-conc
            • Imf-cst-obs-resent-from-conc
            • Imf-cst-obs-resent-date-conc
            • Imf-cst-obs-phrase-list-conc
            • Imf-cst-obs-in-reply-to-conc
            • Imf-cst-obs-id-right-conc-rep-elem
            • Imf-cst-obs-id-left-conc-rep-elem
            • Imf-cst-obs-fields-conc
            • Imf-cst-obs-dtext-conc2-rep-elem
            • Imf-cst-obs-dtext-conc2-rep
            • Imf-cst-obs-dtext-conc1-rep-elem
            • Imf-cst-obs-dtext-conc1-rep
            • Imf-cst-mailbox-conc2-rep-elem
            • Imf-cst-mailbox-conc1-rep-elem
            • Imf-cst-local-part-conc3-rep
            • Imf-cst-local-part-conc3
            • Imf-cst-local-part-conc2-rep
            • Imf-cst-local-part-conc2
            • Imf-cst-local-part-conc1-rep
            • Imf-cst-local-part-conc1
            • Imf-cst-id-right-conc3-rep-elem
            • Imf-cst-id-right-conc3-rep
            • Imf-cst-id-right-conc2-rep-elem
            • Imf-cst-id-right-conc2-rep
            • Imf-cst-id-right-conc1-rep-elem
            • Imf-cst-id-right-conc1-rep
            • Imf-cst-id-left-conc2-rep-elem
            • Imf-cst-id-left-conc1-rep-elem
            • Imf-cst-group-list-conc3-rep
            • Imf-cst-group-list-conc3
            • Imf-cst-group-list-conc2-rep
            • Imf-cst-group-list-conc2
            • Imf-cst-group-list-conc1-rep
            • Imf-cst-group-list-conc1
            • Imf-cst-domain-conc3-rep-elem
            • Imf-cst-domain-conc2-rep-elem
            • Imf-cst-domain-conc1-rep-elem
            • Imf-cst-display-name-conc-rep-elem
            • Imf-cst-ccontent-conc3-rep-elem
            • Imf-cst-ccontent-conc3-rep
            • Imf-cst-ccontent-conc2-rep-elem
            • Imf-cst-ccontent-conc2-rep
            • Imf-cst-ccontent-conc1-rep-elem
            • Imf-cst-ccontent-conc1-rep
            • Imf-cst-address-conc2-rep-elem
            • Imf-cst-address-conc1-rep-elem
            • Imf-cst-wsp-conc2-rep-elem
            • Imf-cst-wsp-conc1-rep-elem
            • Imf-cst-word-conc2-rep-elem
            • Imf-cst-word-conc2-rep
            • Imf-cst-word-conc1-rep-elem
            • Imf-cst-time-of-day-conc
            • Imf-cst-resent-sender-conc
            • Imf-cst-resent-msg-id-conc
            • Imf-cst-resent-from-conc
            • Imf-cst-resent-date-conc
            • Imf-cst-resent-bcc-conc
            • Imf-cst-quoted-string-conc
            • Imf-cst-qcontent-conc2
            • Imf-cst-qcontent-conc1
            • Imf-cst-optional-field-conc
            • Imf-cst-obs-unstruct-conc
            • Imf-cst-obs-subject-conc
            • Imf-cst-obs-resent-to-conc
            • Imf-cst-obs-resent-send-conc
            • Imf-cst-obs-resent-mid-conc
            • Imf-cst-obs-resent-cc-conc
            • Imf-cst-obs-resent-bcc-conc
            • Imf-cst-obs-reply-to-conc
            • Imf-cst-obs-references-conc
            • Imf-cst-obs-received-conc
            • Imf-cst-obs-qtext-conc-rep-elem
            • Imf-cst-obs-qtext-conc-rep
            • Imf-cst-obs-orig-date-conc
            • Imf-cst-obs-optional-conc
            • Imf-cst-obs-message-id-conc
            • Imf-cst-obs-mbox-list-conc
            • Imf-cst-obs-local-part-conc
            • Imf-cst-obs-keywords-conc
            • Imf-cst-obs-id-right-conc-rep
            • Imf-cst-obs-id-right-conc
            • Imf-cst-obs-id-left-conc-rep
            • Imf-cst-obs-group-list-conc
            • Imf-cst-obs-dtext-conc2
            • Imf-cst-obs-dtext-conc1
            • Imf-cst-obs-domain-list-conc
            • Imf-cst-obs-day-of-week-conc
            • Imf-cst-obs-ctext-conc-rep-elem
            • Imf-cst-obs-ctext-conc-rep
            • Imf-cst-obs-comments-conc
            • Imf-cst-obs-angle-addr-conc
            • Imf-cst-obs-addr-list-conc
            • Imf-cst-no-fold-literal-conc
            • Imf-cst-mailbox-conc2-rep
            • Imf-cst-mailbox-conc2
            • Imf-cst-mailbox-conc1-rep
            • Imf-cst-mailbox-conc1
            • Imf-cst-in-reply-to-conc
            • Imf-cst-id-right-conc3
            • Imf-cst-id-right-conc2
            • Imf-cst-id-right-conc1
            • Imf-cst-id-left-conc2-rep
            • Imf-cst-id-left-conc2
            • Imf-cst-id-left-conc1-rep
            • Imf-cst-id-left-conc1
            • Imf-cst-fields-conc
            • Imf-cst-dot-atom-text-conc
            • Imf-cst-domain-literal-conc
            • Imf-cst-domain-conc3-rep
            • Imf-cst-domain-conc3
            • Imf-cst-domain-conc2-rep
            • Imf-cst-domain-conc2
            • Imf-cst-domain-conc1-rep
            • Imf-cst-domain-conc1
            • Imf-cst-display-name-conc-rep
            • Imf-cst-display-name-conc
            • Imf-cst-ccontent-conc3
            • Imf-cst-ccontent-conc2
            • Imf-cst-ccontent-conc1
            • Imf-cst-address-conc2-rep
            • Imf-cst-address-conc2
            • Imf-cst-address-conc1-rep
            • Imf-cst-address-conc1
            • Imf-cst-wsp-conc2-rep
            • Imf-cst-wsp-conc2
            • Imf-cst-wsp-conc1-rep
            • Imf-cst-wsp-conc1
            • Imf-cst-word-conc2
            • Imf-cst-word-conc1-rep
            • Imf-cst-word-conc1
            • Imf-cst-vchar-conc-rep-elem
            • Imf-cst-vchar-conc-rep
            • Imf-cst-subject-conc
            • Imf-cst-sp-conc-rep-elem
            • Imf-cst-return-conc
            • Imf-cst-resent-to-conc
            • Imf-cst-resent-cc-conc
            • Imf-cst-reply-to-conc
            • Imf-cst-references-conc
            • Imf-cst-received-conc
            • Imf-cst-orig-date-conc
            • Imf-cst-obs-year-conc
            • Imf-cst-obs-to-conc
            • Imf-cst-obs-sender-conc
            • Imf-cst-obs-second-conc
            • Imf-cst-obs-route-conc
            • Imf-cst-obs-return-conc
            • Imf-cst-obs-qtext-conc
            • Imf-cst-obs-qp-conc
            • Imf-cst-obs-phrase-conc
            • Imf-cst-obs-minute-conc
            • Imf-cst-obs-id-left-conc
            • Imf-cst-obs-hour-conc
            • Imf-cst-obs-fws-conc
            • Imf-cst-obs-from-conc
            • Imf-cst-obs-domain-conc
            • Imf-cst-obs-day-conc
            • Imf-cst-obs-ctext-conc
            • Imf-cst-obs-cc-conc
            • Imf-cst-obs-body-conc
            • Imf-cst-obs-bcc-conc
            • Imf-cst-name-addr-conc
            • Imf-cst-msg-id-conc
            • Imf-cst-message-id-conc
            • Imf-cst-message-conc
            • Imf-cst-lf-conc-rep-elem
            • Imf-cst-keywords-conc
            • Imf-cst-htab-conc-rep-elem
            • Imf-cst-htab-conc-rep
            • Imf-cst-group-conc
            • Imf-cst-field-name-conc
            • Imf-cst-dquote-conc-rep-elem
            • Imf-cst-dquote-conc-rep
            • Imf-cst-dot-atom-conc
            • Imf-cst-digit-conc-rep-elem
            • Imf-cst-digit-conc-rep
            • Imf-cst-date-time-conc
            • Imf-cst-cr-conc-rep-elem
            • Imf-cst-comments-conc
            • Imf-cst-comment-conc
            • Imf-cst-addr-spec-conc
            • Imf-cst-vchar-conc
            • Imf-cst-trace-conc
            • Imf-cst-to-conc
            • Imf-cst-time-conc
            • Imf-cst-sp-conc-rep
            • Imf-cst-sp-conc
            • Imf-cst-sender-conc
            • Imf-cst-lf-conc-rep
            • Imf-cst-lf-conc
            • Imf-cst-htab-conc
            • Imf-cst-from-conc
            • Imf-cst-dquote-conc
            • Imf-cst-digit-conc
            • Imf-cst-date-conc
            • Imf-cst-crlf-conc
            • Imf-cst-cr-conc-rep
            • Imf-cst-cr-conc
            • Imf-cst-cc-conc
            • Imf-cst-bcc-conc
            • Imf-cst-atom-conc
            • *imf-grammar-rules*
            • Imf-cst-%x61-7a-nat
            • Imf-cst-%x41-5a-nat
            • Imf-cst-%x30-39-nat
            • Imf-cst-%x21-7e-nat
            • Imf-cst-%d97-105-nat
            • Imf-cst-%d94-126-nat
            • Imf-cst-%d93-126-nat
            • Imf-cst-%d75-90-nat
            • Imf-cst-%d65-73-nat
            • Imf-cst-%d59-126-nat
            • Imf-cst-%d42-91-nat
            • Imf-cst-%d35-91-nat
            • Imf-cst-%d33-90-nat
            • Imf-cst-%d33-57-nat
            • Imf-cst-%d33-39-nat
            • Imf-cst-%d14-31-nat
            • Imf-cst-%d14-127-nat
            • Imf-cst-%d107-122-nat
            • Imf-cst-%d1-9-nat
            • Imf-cst-%d1-8-nat
        • 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
  • Examples

Imf-example

The ABNF grammar of the IMF (Internet Message Format) syntax.

The IMF syntax is specified by RFC 5322.

Subtopics

Imf-cst-received-token-conc?
Imf-cst-local-part-conc?
Imf-cst-id-right-conc?
Imf-cst-group-list-conc?
Imf-cst-domain-conc?
Imf-cst-ccontent-conc?
*all-imf-grammar-rules*
All the IMF grammar rules, including the referenced ABNF core rules.
Imf-cst-list-list-conc-matchp$
Imf-cst-obs-dtext-conc?
Imf-cst-list-list-alt-matchp$
Imf-cst-qcontent-conc?
Imf-cst-mailbox-conc?
Imf-cst-id-left-conc?
Imf-cst-address-conc?
Imf-cst-wsp-conc?
Imf-cst-word-conc?
Imf-cst-list-rep-matchp$
Imf-cst-list-elem-matchp$
Imf-cst-received-token-conc4-rep-elem
Imf-cst-received-token-conc3-rep-elem
Imf-cst-received-token-conc2-rep-elem
Imf-cst-received-token-conc1-rep-elem
Imf-cst-received-token-conc4-rep
Imf-cst-received-token-conc3-rep
Imf-cst-received-token-conc2-rep
Imf-cst-received-token-conc1-rep
Imf-cst-matchp$
Imf-cst-local-part-conc3-rep-elem
Imf-cst-local-part-conc2-rep-elem
Imf-cst-local-part-conc1-rep-elem
Imf-cst-group-list-conc3-rep-elem
Imf-cst-group-list-conc2-rep-elem
Imf-cst-group-list-conc1-rep-elem
Imf-cst-received-token-conc4
Imf-cst-received-token-conc3
Imf-cst-received-token-conc2
Imf-cst-received-token-conc1
Imf-cst-qcontent-conc2-rep-elem
Imf-cst-qcontent-conc2-rep
Imf-cst-qcontent-conc1-rep-elem
Imf-cst-qcontent-conc1-rep
Imf-cst-obs-resent-rply-conc
Imf-cst-obs-resent-from-conc
Imf-cst-obs-resent-date-conc
Imf-cst-obs-phrase-list-conc
Imf-cst-obs-in-reply-to-conc
Imf-cst-obs-id-right-conc-rep-elem
Imf-cst-obs-id-left-conc-rep-elem
Imf-cst-obs-fields-conc
Imf-cst-obs-dtext-conc2-rep-elem
Imf-cst-obs-dtext-conc2-rep
Imf-cst-obs-dtext-conc1-rep-elem
Imf-cst-obs-dtext-conc1-rep
Imf-cst-mailbox-conc2-rep-elem
Imf-cst-mailbox-conc1-rep-elem
Imf-cst-local-part-conc3-rep
Imf-cst-local-part-conc3
Imf-cst-local-part-conc2-rep
Imf-cst-local-part-conc2
Imf-cst-local-part-conc1-rep
Imf-cst-local-part-conc1
Imf-cst-id-right-conc3-rep-elem
Imf-cst-id-right-conc3-rep
Imf-cst-id-right-conc2-rep-elem
Imf-cst-id-right-conc2-rep
Imf-cst-id-right-conc1-rep-elem
Imf-cst-id-right-conc1-rep
Imf-cst-id-left-conc2-rep-elem
Imf-cst-id-left-conc1-rep-elem
Imf-cst-group-list-conc3-rep
Imf-cst-group-list-conc3
Imf-cst-group-list-conc2-rep
Imf-cst-group-list-conc2
Imf-cst-group-list-conc1-rep
Imf-cst-group-list-conc1
Imf-cst-domain-conc3-rep-elem
Imf-cst-domain-conc2-rep-elem
Imf-cst-domain-conc1-rep-elem
Imf-cst-display-name-conc-rep-elem
Imf-cst-ccontent-conc3-rep-elem
Imf-cst-ccontent-conc3-rep
Imf-cst-ccontent-conc2-rep-elem
Imf-cst-ccontent-conc2-rep
Imf-cst-ccontent-conc1-rep-elem
Imf-cst-ccontent-conc1-rep
Imf-cst-address-conc2-rep-elem
Imf-cst-address-conc1-rep-elem
Imf-cst-wsp-conc2-rep-elem
Imf-cst-wsp-conc1-rep-elem
Imf-cst-word-conc2-rep-elem
Imf-cst-word-conc2-rep
Imf-cst-word-conc1-rep-elem
Imf-cst-time-of-day-conc
Imf-cst-resent-sender-conc
Imf-cst-resent-msg-id-conc
Imf-cst-resent-from-conc
Imf-cst-resent-date-conc
Imf-cst-resent-bcc-conc
Imf-cst-quoted-string-conc
Imf-cst-qcontent-conc2
Imf-cst-qcontent-conc1
Imf-cst-optional-field-conc
Imf-cst-obs-unstruct-conc
Imf-cst-obs-subject-conc
Imf-cst-obs-resent-to-conc
Imf-cst-obs-resent-send-conc
Imf-cst-obs-resent-mid-conc
Imf-cst-obs-resent-cc-conc
Imf-cst-obs-resent-bcc-conc
Imf-cst-obs-reply-to-conc
Imf-cst-obs-references-conc
Imf-cst-obs-received-conc
Imf-cst-obs-qtext-conc-rep-elem
Imf-cst-obs-qtext-conc-rep
Imf-cst-obs-orig-date-conc
Imf-cst-obs-optional-conc
Imf-cst-obs-message-id-conc
Imf-cst-obs-mbox-list-conc
Imf-cst-obs-local-part-conc
Imf-cst-obs-keywords-conc
Imf-cst-obs-id-right-conc-rep
Imf-cst-obs-id-right-conc
Imf-cst-obs-id-left-conc-rep
Imf-cst-obs-group-list-conc
Imf-cst-obs-dtext-conc2
Imf-cst-obs-dtext-conc1
Imf-cst-obs-domain-list-conc
Imf-cst-obs-day-of-week-conc
Imf-cst-obs-ctext-conc-rep-elem
Imf-cst-obs-ctext-conc-rep
Imf-cst-obs-comments-conc
Imf-cst-obs-angle-addr-conc
Imf-cst-obs-addr-list-conc
Imf-cst-no-fold-literal-conc
Imf-cst-mailbox-conc2-rep
Imf-cst-mailbox-conc2
Imf-cst-mailbox-conc1-rep
Imf-cst-mailbox-conc1
Imf-cst-in-reply-to-conc
Imf-cst-id-right-conc3
Imf-cst-id-right-conc2
Imf-cst-id-right-conc1
Imf-cst-id-left-conc2-rep
Imf-cst-id-left-conc2
Imf-cst-id-left-conc1-rep
Imf-cst-id-left-conc1
Imf-cst-fields-conc
Imf-cst-dot-atom-text-conc
Imf-cst-domain-literal-conc
Imf-cst-domain-conc3-rep
Imf-cst-domain-conc3
Imf-cst-domain-conc2-rep
Imf-cst-domain-conc2
Imf-cst-domain-conc1-rep
Imf-cst-domain-conc1
Imf-cst-display-name-conc-rep
Imf-cst-display-name-conc
Imf-cst-ccontent-conc3
Imf-cst-ccontent-conc2
Imf-cst-ccontent-conc1
Imf-cst-address-conc2-rep
Imf-cst-address-conc2
Imf-cst-address-conc1-rep
Imf-cst-address-conc1
Imf-cst-wsp-conc2-rep
Imf-cst-wsp-conc2
Imf-cst-wsp-conc1-rep
Imf-cst-wsp-conc1
Imf-cst-word-conc2
Imf-cst-word-conc1-rep
Imf-cst-word-conc1
Imf-cst-vchar-conc-rep-elem
Imf-cst-vchar-conc-rep
Imf-cst-subject-conc
Imf-cst-sp-conc-rep-elem
Imf-cst-return-conc
Imf-cst-resent-to-conc
Imf-cst-resent-cc-conc
Imf-cst-reply-to-conc
Imf-cst-references-conc
Imf-cst-received-conc
Imf-cst-orig-date-conc
Imf-cst-obs-year-conc
Imf-cst-obs-to-conc
Imf-cst-obs-sender-conc
Imf-cst-obs-second-conc
Imf-cst-obs-route-conc
Imf-cst-obs-return-conc
Imf-cst-obs-qtext-conc
Imf-cst-obs-qp-conc
Imf-cst-obs-phrase-conc
Imf-cst-obs-minute-conc
Imf-cst-obs-id-left-conc
Imf-cst-obs-hour-conc
Imf-cst-obs-fws-conc
Imf-cst-obs-from-conc
Imf-cst-obs-domain-conc
Imf-cst-obs-day-conc
Imf-cst-obs-ctext-conc
Imf-cst-obs-cc-conc
Imf-cst-obs-body-conc
Imf-cst-obs-bcc-conc
Imf-cst-name-addr-conc
Imf-cst-msg-id-conc
Imf-cst-message-id-conc
Imf-cst-message-conc
Imf-cst-lf-conc-rep-elem
Imf-cst-keywords-conc
Imf-cst-htab-conc-rep-elem
Imf-cst-htab-conc-rep
Imf-cst-group-conc
Imf-cst-field-name-conc
Imf-cst-dquote-conc-rep-elem
Imf-cst-dquote-conc-rep
Imf-cst-dot-atom-conc
Imf-cst-digit-conc-rep-elem
Imf-cst-digit-conc-rep
Imf-cst-date-time-conc
Imf-cst-cr-conc-rep-elem
Imf-cst-comments-conc
Imf-cst-comment-conc
Imf-cst-addr-spec-conc
Imf-cst-vchar-conc
Imf-cst-trace-conc
Imf-cst-to-conc
Imf-cst-time-conc
Imf-cst-sp-conc-rep
Imf-cst-sp-conc
Imf-cst-sender-conc
Imf-cst-lf-conc-rep
Imf-cst-lf-conc
Imf-cst-htab-conc
Imf-cst-from-conc
Imf-cst-dquote-conc
Imf-cst-digit-conc
Imf-cst-date-conc
Imf-cst-crlf-conc
Imf-cst-cr-conc-rep
Imf-cst-cr-conc
Imf-cst-cc-conc
Imf-cst-bcc-conc
Imf-cst-atom-conc
*imf-grammar-rules*
The IMF grammar rules from RFC 5322.
Imf-cst-%x61-7a-nat
Imf-cst-%x41-5a-nat
Imf-cst-%x30-39-nat
Imf-cst-%x21-7e-nat
Imf-cst-%d97-105-nat
Imf-cst-%d94-126-nat
Imf-cst-%d93-126-nat
Imf-cst-%d75-90-nat
Imf-cst-%d65-73-nat
Imf-cst-%d59-126-nat
Imf-cst-%d42-91-nat
Imf-cst-%d35-91-nat
Imf-cst-%d33-90-nat
Imf-cst-%d33-57-nat
Imf-cst-%d33-39-nat
Imf-cst-%d14-31-nat
Imf-cst-%d14-127-nat
Imf-cst-%d107-122-nat
Imf-cst-%d1-9-nat
Imf-cst-%d1-8-nat