Body.Empty

Represents an always-empty, already-closed body handle.

structure Std.Http.Body.Empty : Type

An empty body handle.

@[implicit_reducible]

instance Std.Http.Body.instInhabitedEmpty : Inhabited Empty

Equations

• Std.Http.Body.instInhabitedEmpty = { default := Std.Http.Body.instInhabitedEmpty.default }

def Std.Http.Body.instInhabitedEmpty.default : Empty

Equations

• Std.Http.Body.instInhabitedEmpty.default = { }

def Std.Http.Body.instBEqEmpty.beq : Empty → Empty → Bool

Equations

• Std.Http.Body.instBEqEmpty.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Std.Http.Body.instBEqEmpty : BEq Empty

Equations

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

@[inline]

def Std.Http.Body.Empty.recv : Empty → Internal.IO.Async.Async (Option Chunk)

Receives from an empty body, always returning end-of-stream.

Equations

• x✝.recv = pure none

@[inline]

def Std.Http.Body.Empty.close : Empty → Internal.IO.Async.Async Unit

Closes an empty body (no-op).

Equations

• x✝.close = pure ()

@[inline]

def Std.Http.Body.Empty.isClosed : Empty → Internal.IO.Async.Async Bool

Empty bodies are always closed for reading.

Equations

• x✝.isClosed = pure true

@[inline]

def Std.Http.Body.Empty.recvSelector : Empty → Internal.IO.Async.Selector (Option Chunk)

Selector that immediately resolves with end-of-stream for an empty body.

Equations

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

@[implicit_reducible]

instance Std.Http.Body.instEmpty : Body Empty

Equations

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

@[implicit_reducible]

instance Std.Http.Body.instCoeEmptyAny : Coe Empty Any

Equations

• Std.Http.Body.instCoeEmptyAny = { coe := Std.Http.Body.Any.ofBody }

@[implicit_reducible]

instance Std.Http.Body.instCoeResponseEmptyAny : Coe (Response Empty) (Response Any)

Equations

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

@[implicit_reducible]

instance Std.Http.Body.instCoeContextAsyncResponseEmptyAny : Coe (Internal.IO.Async.ContextAsync (Response Empty)) (Internal.IO.Async.ContextAsync (Response Any))

Equations

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

@[implicit_reducible]

instance Std.Http.Body.instCoeAsyncResponseEmptyContextAsyncAny : Coe (Internal.IO.Async.Async (Response Empty)) (Internal.IO.Async.ContextAsync (Response Any))

Equations

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

def Std.Http.Request.Builder.empty (builder : Builder) : Internal.IO.Async.Async (Request Body.Empty)

Builds a request with no body.

Equations

• builder.empty = pure (builder.body { })

def Std.Http.Response.Builder.empty (builder : Builder) : Internal.IO.Async.Async (Response Body.Empty)

Builds a response with no body.

Equations

• builder.empty = pure (builder.body { })