Body.Length

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

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.

def Std.Http.Body.instReprLength.repr : Length → Nat → Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Std.Http.Body.instReprLength : Repr Length

Equations

• Std.Http.Body.instReprLength = { reprPrec := Std.Http.Body.instReprLength.repr }

def Std.Http.Body.instBEqLength.beq : Length → Length → Bool

Equations

• Std.Http.Body.instBEqLength.beq Std.Http.Body.Length.chunked Std.Http.Body.Length.chunked = true
• Std.Http.Body.instBEqLength.beq (Std.Http.Body.Length.fixed a) (Std.Http.Body.Length.fixed b) = (a == b)
• Std.Http.Body.instBEqLength.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Std.Http.Body.instBEqLength : BEq Length

Equations

• Std.Http.Body.instBEqLength = { beq := Std.Http.Body.instBEqLength.beq }

@[inline]

def Std.Http.Body.Length.isChunked : Length → Bool

Checks if the Length is chunked.

Equations

• Std.Http.Body.Length.chunked.isChunked = true
• x✝.isChunked = false

@[inline]

def Std.Http.Body.Length.isFixed : Length → Bool

Checks if the Length is a fixed size.

Equations

• (Std.Http.Body.Length.fixed n).isFixed = true
• x✝.isFixed = false