HTTP/1.1 Events

This module defines the events that can occur during HTTP/1.1 message processing, including header completion and control/error signals.

inductive Std.Http.Protocol.H1.Event (dir : Direction) : Type

Events emitted during HTTP message processing.

• endHeaders {dir : Direction} (head : Message.Head dir) : Event dir

  Indicates that all headers have been successfully parsed.

• needMoreData {dir : Direction} (size : Option Nat) : Event dir

  Signals that additional input data is required to continue processing.

• failed {dir : Direction} (err : Error) : Event dir

  Indicates a failure during parsing or processing.

• close {dir : Direction} : Event dir

  Requests that the connection be closed.

• closeBody {dir : Direction} : Event dir

  The body should be closed.

• needAnswer {dir : Direction} : Event dir

  Indicates that a response is required.

• next {dir : Direction} : Event dir

  Indicates readiness to process the next message.

• continue {dir : Direction} : Event dir

  Signals that an Expect: 100-continue decision is pending.

@[implicit_reducible]

instance Std.Http.Protocol.H1.instInhabitedEvent {a✝ : Direction} : Inhabited (Event a✝)

Equations

• Std.Http.Protocol.H1.instInhabitedEvent = { default := Std.Http.Protocol.H1.instInhabitedEvent.default }

@[implicit_reducible]

instance Std.Http.Protocol.H1.instReprEvent {dir✝ : Direction} : Repr (Event dir✝)

Equations

• Std.Http.Protocol.H1.instReprEvent = { reprPrec := Std.Http.Protocol.H1.instReprEvent.repr }

def Std.Http.Protocol.H1.instReprEvent.repr {dir✝ : Direction} : Event dir✝ → Nat → Format

Equations

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