Documentation

Std.Internal.Http.Data.Body.Length

Body.Length #

This module defines the Length type, that represents the Content-Length or Transfer-Encoding of an HTTP request or response.

source
inductive Std.Http.Body.Length :
Type

Size of the body of a response or request.

  • chunked : Length

    Indicates that the HTTP message body uses chunked transfer encoding.

  • fixed (n : Nat) : Length

    Indicates that the HTTP message body has a fixed, known length, as specified by the Content-Length header.

Instances For
    source
    def Std.Http.Body.instReprLength.repr :
    Length → Nat → Format
    Instances For
      source
      @[implicit_reducible]
      instance Std.Http.Body.instReprLength :
      Repr Length
      source
      def Std.Http.Body.instBEqLength.beq :
      Length → Length → Bool
      Instances For
        source
        @[implicit_reducible]
        instance Std.Http.Body.instBEqLength :
        BEq Length
        source
        @[inline]
        def Std.Http.Body.Length.isChunked :
        Length → Bool

        Checks if the Length is chunked.

        Instances For
          source
          @[inline]
          def Std.Http.Body.Length.isFixed :
          Length → Bool

          Checks if the Length is a fixed size.

          Instances For