• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Acre
    • Milawa
    • Smtlink
    • Aleobft
    • Abnf
      • Deftreeops
      • Defdefparse
      • Defgrammar
      • Abnf-tree-utilities
      • Notation
      • Grammar-parser
      • Meta-circular-validation
      • Parsing-primitives-defresult
      • Parsing-primitives-seq
      • Operations
      • Examples
        • Pdf-example
        • Smtp-example
        • Imap-example
        • Http-example
          • *all-http-grammar-rules*
          • *all-http-message-grammar-rules*
          • Http-cst-request-target-conc?
          • Http-cst-uri-host-conc?
          • Http-cst-start-line-conc?
          • Http-cst-list-list-conc-matchp$
          • Http-cst-list-list-alt-matchp$
          • Http-cst-field-vchar-conc?
          • Http-cst-chunk-ext-val-conc?
          • Http-cst-list-rep-matchp$
          • Http-cst-list-elem-matchp$
          • Http-cst-request-target-conc4-rep-elem
          • Http-cst-request-target-conc3-rep-elem
          • Http-cst-request-target-conc2-rep-elem
          • Http-cst-request-target-conc1-rep-elem
          • Http-cst-chunk-ext-val-conc2-rep-elem
          • Http-cst-chunk-ext-val-conc1-rep-elem
          • Http-cst-start-line-conc2-rep-elem
          • Http-cst-start-line-conc1-rep-elem
          • Http-cst-request-target-conc4-rep
          • Http-cst-request-target-conc4
          • Http-cst-request-target-conc3-rep
          • Http-cst-request-target-conc3
          • Http-cst-request-target-conc2-rep
          • Http-cst-request-target-conc2
          • Http-cst-request-target-conc1-rep
          • Http-cst-request-target-conc1
          • Http-cst-protocol-version-conc-rep-elem
          • Http-cst-matchp$
          • Http-cst-field-vchar-conc2-rep-elem
          • Http-cst-field-vchar-conc2-rep
          • Http-cst-field-vchar-conc1-rep-elem
          • Http-cst-field-vchar-conc1-rep
          • Http-cst-connection-option-conc-rep-elem
          • Http-cst-connection-option-conc-rep
          • Http-cst-chunk-ext-val-conc2-rep
          • Http-cst-chunk-ext-val-conc1-rep
          • Http-cst-uri-host-conc3-rep-elem
          • Http-cst-uri-host-conc3-rep
          • Http-cst-uri-host-conc2-rep-elem
          • Http-cst-uri-host-conc2-rep
          • Http-cst-uri-host-conc1-rep-elem
          • Http-cst-uri-host-conc1-rep
          • Http-cst-transfer-parameter-conc
          • Http-cst-transfer-extension-conc
          • Http-cst-transfer-encoding-conc
          • Http-cst-start-line-conc2-rep
          • Http-cst-start-line-conc2
          • Http-cst-start-line-conc1-rep
          • Http-cst-start-line-conc1
          • Http-cst-received-protocol-conc
          • Http-cst-protocol-version-conc-rep
          • Http-cst-protocol-version-conc
          • Http-cst-protocol-name-conc-rep-elem
          • Http-cst-protocol-name-conc-rep
          • Http-cst-field-vchar-conc2
          • Http-cst-field-vchar-conc1
          • Http-cst-field-name-conc-rep-elem
          • Http-cst-connection-option-conc
          • Http-cst-chunk-ext-val-conc2
          • Http-cst-chunk-ext-val-conc1
          • Http-cst-chunk-ext-name-conc-rep-elem
          • Http-cst-chunk-ext-name-conc-rep
          • Http-cst-authority-form-conc-rep-elem
          • Http-cst-authority-form-conc-rep
          • Http-cst-asterisk-form-conc-rep-elem
          • Http-cst-asterisk-form-conc-rep
          • Http-cst-absolute-form-conc-rep-elem
          • Http-cst-absolute-form-conc-rep
          • Http-cst-uri-host-conc3
          • Http-cst-uri-host-conc2
          • Http-cst-uri-host-conc1
          • Http-cst-trailer-part-conc
          • Http-cst-status-line-conc
          • Http-cst-status-code-conc
          • Http-cst-segment-nz-nc-conc
          • Http-cst-request-line-conc
          • Http-cst-reason-phrase-conc
          • Http-cst-quoted-string-conc
          • Http-cst-quoted-pair-conc
          • Http-cst-pseudonym-conc-rep-elem
          • Http-cst-pseudonym-conc-rep
          • Http-cst-protocol-name-conc
          • Http-cst-pct-encoded-conc
          • Http-cst-path-rootless-conc
          • Http-cst-path-noscheme-conc
          • Http-cst-path-absolute-conc
          • Http-cst-path-abempty-conc
          • Http-cst-partial-uri-conc
          • Http-cst-origin-form-conc
          • Http-cst-obs-text-conc-rep-elem
          • Http-cst-obs-text-conc-rep
          • Http-cst-method-conc-rep-elem
          • Http-cst-message-body-conc
          • Http-cst-last-chunk-conc
          • Http-cst-ipv4address-conc
          • Http-cst-ip-literal-conc
          • Http-cst-http-version-conc
          • Http-cst-http-name-conc-rep-elem
          • Http-cst-http-name-conc-rep
          • Http-cst-http-message-conc
          • Http-cst-header-field-conc
          • Http-cst-field-value-conc
          • Http-cst-field-name-conc-rep
          • Http-cst-field-content-conc
          • Http-cst-dquote-conc-rep-elem
          • Http-cst-content-length-conc
          • Http-cst-connection-conc
          • Http-cst-chunked-body-conc
          • Http-cst-chunk-ext-name-conc
          • Http-cst-authority-form-conc
          • Http-cst-asterisk-form-conc
          • Http-cst-absolute-uri-conc
          • Http-cst-absolute-path-conc
          • Http-cst-absolute-form-conc
          • Http-cst-via-conc
          • Http-cst-vchar-conc-rep-elem
          • Http-cst-vchar-conc-rep
          • Http-cst-userinfo-conc
          • Http-cst-upgrade-conc
          • Http-cst-trailer-conc
          • Http-cst-te-conc-rep-elem
          • Http-cst-te-conc-rep
          • Http-cst-t-ranking-conc
          • Http-cst-sp-conc-rep-elem
          • Http-cst-segment-nz-conc
          • Http-cst-segment-conc
          • Http-cst-scheme-conc
          • Http-cst-reg-name-conc
          • Http-cst-pseudonym-conc
          • Http-cst-protocol-conc
          • Http-cst-path-empty-conc
          • Http-cst-octet-conc-rep-elem
          • Http-cst-octet-conc-rep
          • Http-cst-obs-text-conc
          • Http-cst-obs-fold-conc
          • Http-cst-method-conc-rep
          • Http-cst-method-conc
          • Http-cst-lf-conc-rep-elem
          • Http-cst-ipvfuture-conc
          • Http-cst-https-uri-conc
          • Http-cst-http-uri-conc
          • Http-cst-http-name-conc
          • Http-cst-htab-conc-rep-elem
          • Http-cst-htab-conc-rep
          • Http-cst-fragment-conc
          • Http-cst-field-name-conc
          • Http-cst-dquote-conc-rep
          • Http-cst-dquote-conc
          • Http-cst-digit-conc-rep-elem
          • Http-cst-digit-conc-rep
          • Http-cst-cr-conc-rep-elem
          • Http-cst-comment-conc
          • Http-cst-chunk-size-conc
          • Http-cst-chunk-ext-conc
          • Http-cst-chunk-data-conc
          • Http-cst-chunk-conc
          • Http-cst-bws-conc-rep-elem
          • Http-cst-bws-conc-rep
          • Http-cst-authority-conc
          • *http-grammar-rules*
          • Http-cst-vchar-conc
          • Http-cst-token-conc
          • Http-cst-te-conc
          • Http-cst-sp-conc-rep
          • Http-cst-sp-conc
          • Http-cst-rws-conc
          • Http-cst-query-conc
          • Http-cst-port-conc
          • Http-cst-ows-conc
          • Http-cst-octet-conc
          • Http-cst-lf-conc-rep
          • Http-cst-lf-conc
          • Http-cst-htab-conc
          • Http-cst-host-conc
          • Http-cst-h16-conc
          • Http-cst-digit-conc
          • Http-cst-crlf-conc
          • Http-cst-cr-conc-rep
          • Http-cst-cr-conc
          • Http-cst-bws-conc
          • Http-cst-%x80-ff-nat
          • Http-cst-%x61-7a-nat
          • Http-cst-%x5d-7e-nat
          • Http-cst-%x41-5a-nat
          • Http-cst-%x31-39-nat
          • Http-cst-%x30-39-nat
          • Http-cst-%x30-35-nat
          • Http-cst-%x30-34-nat
          • Http-cst-%x2a-5b-nat
          • Http-cst-%x23-5b-nat
          • Http-cst-%x21-7e-nat
          • Http-cst-%x21-27-nat
          • Http-cst-%x0-ff-nat
        • Uri-example
        • Imf-example
      • Differences-with-paper
      • Grammar-printer
      • Parsing-tools
    • Vwsim
    • Isar
    • Wp-gen
    • Dimacs-reader
    • Pfcs
    • Legacy-defrstobj
    • Proof-checker-array
    • Soft
    • Farray
    • Rp-rewriter
    • Instant-runoff-voting
    • Imp-language
    • Sidekick
    • Leftist-trees
    • C
    • Java
    • Taspi
    • Bitcoin
    • Des
    • Ethereum
    • X86isa
    • Sha-2
    • Yul
    • Riscv
    • Zcash
    • Proof-checker-itp13
    • Regex
    • ACL2-programming-language
    • Json
    • Jfkr
    • Equational
    • Cryptography
    • Poseidon
    • Where-do-i-place-my-book
    • Bigmems
    • Builtins
    • Axe
    • Execloader
    • Solidity
    • Leo
    • Paco
    • Concurrent-programs
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Examples

Http-example

The ABNF grammar of the HTTP (Hypertext Transfer Protocol) 1.1 syntax.

The HTTP 1.1 syntax is specified by RFC 7230.

Subtopics

*all-http-grammar-rules*

All the HTTP grammar rules, including the referenced URI rules and ABNF core rules.

*all-http-message-grammar-rules*

All the HTTP grammar rules that define the first-level structure of messages.

Http-cst-request-target-conc?

Http-cst-uri-host-conc?

Http-cst-start-line-conc?

Http-cst-list-list-conc-matchp$

Http-cst-list-list-alt-matchp$

Http-cst-field-vchar-conc?

Http-cst-chunk-ext-val-conc?

Http-cst-list-rep-matchp$

Http-cst-list-elem-matchp$

Http-cst-request-target-conc4-rep-elem

Http-cst-request-target-conc3-rep-elem

Http-cst-request-target-conc2-rep-elem

Http-cst-request-target-conc1-rep-elem

Http-cst-chunk-ext-val-conc2-rep-elem

Http-cst-chunk-ext-val-conc1-rep-elem

Http-cst-start-line-conc2-rep-elem

Http-cst-start-line-conc1-rep-elem

Http-cst-request-target-conc4-rep

Http-cst-request-target-conc4

Http-cst-request-target-conc3-rep

Http-cst-request-target-conc3

Http-cst-request-target-conc2-rep

Http-cst-request-target-conc2

Http-cst-request-target-conc1-rep

Http-cst-request-target-conc1

Http-cst-protocol-version-conc-rep-elem

Http-cst-matchp$

Http-cst-field-vchar-conc2-rep-elem

Http-cst-field-vchar-conc2-rep

Http-cst-field-vchar-conc1-rep-elem

Http-cst-field-vchar-conc1-rep

Http-cst-connection-option-conc-rep-elem

Http-cst-connection-option-conc-rep

Http-cst-chunk-ext-val-conc2-rep

Http-cst-chunk-ext-val-conc1-rep

Http-cst-uri-host-conc3-rep-elem

Http-cst-uri-host-conc3-rep

Http-cst-uri-host-conc2-rep-elem

Http-cst-uri-host-conc2-rep

Http-cst-uri-host-conc1-rep-elem

Http-cst-uri-host-conc1-rep

Http-cst-transfer-parameter-conc

Http-cst-transfer-extension-conc

Http-cst-transfer-encoding-conc

Http-cst-start-line-conc2-rep

Http-cst-start-line-conc2

Http-cst-start-line-conc1-rep

Http-cst-start-line-conc1

Http-cst-received-protocol-conc

Http-cst-protocol-version-conc-rep

Http-cst-protocol-version-conc

Http-cst-protocol-name-conc-rep-elem

Http-cst-protocol-name-conc-rep

Http-cst-field-vchar-conc2

Http-cst-field-vchar-conc1

Http-cst-field-name-conc-rep-elem

Http-cst-connection-option-conc

Http-cst-chunk-ext-val-conc2

Http-cst-chunk-ext-val-conc1

Http-cst-chunk-ext-name-conc-rep-elem

Http-cst-chunk-ext-name-conc-rep

Http-cst-authority-form-conc-rep-elem

Http-cst-authority-form-conc-rep

Http-cst-asterisk-form-conc-rep-elem

Http-cst-asterisk-form-conc-rep

Http-cst-absolute-form-conc-rep-elem

Http-cst-absolute-form-conc-rep

Http-cst-uri-host-conc3

Http-cst-uri-host-conc2

Http-cst-uri-host-conc1

Http-cst-trailer-part-conc

Http-cst-status-line-conc

Http-cst-status-code-conc

Http-cst-segment-nz-nc-conc

Http-cst-request-line-conc

Http-cst-reason-phrase-conc

Http-cst-quoted-string-conc

Http-cst-quoted-pair-conc

Http-cst-pseudonym-conc-rep-elem

Http-cst-pseudonym-conc-rep

Http-cst-protocol-name-conc

Http-cst-pct-encoded-conc

Http-cst-path-rootless-conc

Http-cst-path-noscheme-conc

Http-cst-path-absolute-conc

Http-cst-path-abempty-conc

Http-cst-partial-uri-conc

Http-cst-origin-form-conc

Http-cst-obs-text-conc-rep-elem

Http-cst-obs-text-conc-rep

Http-cst-method-conc-rep-elem

Http-cst-message-body-conc

Http-cst-last-chunk-conc

Http-cst-ipv4address-conc

Http-cst-ip-literal-conc

Http-cst-http-version-conc

Http-cst-http-name-conc-rep-elem

Http-cst-http-name-conc-rep

Http-cst-http-message-conc

Http-cst-header-field-conc

Http-cst-field-value-conc

Http-cst-field-name-conc-rep

Http-cst-field-content-conc

Http-cst-dquote-conc-rep-elem

Http-cst-content-length-conc

Http-cst-connection-conc

Http-cst-chunked-body-conc

Http-cst-chunk-ext-name-conc

Http-cst-authority-form-conc

Http-cst-asterisk-form-conc

Http-cst-absolute-uri-conc

Http-cst-absolute-path-conc

Http-cst-absolute-form-conc

Http-cst-via-conc

Http-cst-vchar-conc-rep-elem

Http-cst-vchar-conc-rep

Http-cst-userinfo-conc

Http-cst-upgrade-conc

Http-cst-trailer-conc

Http-cst-te-conc-rep-elem

Http-cst-te-conc-rep

Http-cst-t-ranking-conc

Http-cst-sp-conc-rep-elem

Http-cst-segment-nz-conc

Http-cst-segment-conc

Http-cst-scheme-conc

Http-cst-reg-name-conc

Http-cst-pseudonym-conc

Http-cst-protocol-conc

Http-cst-path-empty-conc

Http-cst-octet-conc-rep-elem

Http-cst-octet-conc-rep

Http-cst-obs-text-conc

Http-cst-obs-fold-conc

Http-cst-method-conc-rep

Http-cst-method-conc

Http-cst-lf-conc-rep-elem

Http-cst-ipvfuture-conc

Http-cst-https-uri-conc

Http-cst-http-uri-conc

Http-cst-http-name-conc

Http-cst-htab-conc-rep-elem

Http-cst-htab-conc-rep

Http-cst-fragment-conc

Http-cst-field-name-conc

Http-cst-dquote-conc-rep

Http-cst-dquote-conc

Http-cst-digit-conc-rep-elem

Http-cst-digit-conc-rep

Http-cst-cr-conc-rep-elem

Http-cst-comment-conc

Http-cst-chunk-size-conc

Http-cst-chunk-ext-conc

Http-cst-chunk-data-conc

Http-cst-chunk-conc

Http-cst-bws-conc-rep-elem

Http-cst-bws-conc-rep

Http-cst-authority-conc

*http-grammar-rules*

The HTTP grammar rules from RFC 7230.

Http-cst-vchar-conc

Http-cst-token-conc

Http-cst-te-conc

Http-cst-sp-conc-rep

Http-cst-sp-conc

Http-cst-rws-conc

Http-cst-query-conc

Http-cst-port-conc

Http-cst-ows-conc

Http-cst-octet-conc

Http-cst-lf-conc-rep

Http-cst-lf-conc

Http-cst-htab-conc

Http-cst-host-conc

Http-cst-h16-conc

Http-cst-digit-conc

Http-cst-crlf-conc

Http-cst-cr-conc-rep

Http-cst-cr-conc

Http-cst-bws-conc

Http-cst-%x80-ff-nat

Http-cst-%x61-7a-nat

Http-cst-%x5d-7e-nat

Http-cst-%x41-5a-nat

Http-cst-%x31-39-nat

Http-cst-%x30-39-nat

Http-cst-%x30-35-nat

Http-cst-%x30-34-nat

Http-cst-%x2a-5b-nat

Http-cst-%x23-5b-nat

Http-cst-%x21-7e-nat

Http-cst-%x21-27-nat

Http-cst-%x0-ff-nat