Version

This module defines Version, the set of HTTP protocol versions modeled by this library.

Reference: https://httpwg.org/specs/rfc9110.html#protocol.version

inductive Std.Http.Version : Type

HTTP protocol versions modeled by this library.

Reference: https://httpwg.org/specs/rfc9110.html#protocol.version

• v10 : Version

  HTTP/1.0

• v11 : Version

  HTTP/1.1

• v20 : Version

  HTTP/2.0

• v30 : Version

  HTTP/3.0

def Std.Http.instReprVersion.repr : Version → Nat → Format

Equations

• Std.Http.instReprVersion.repr Std.Http.Version.v10 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Version.v10")).group prec✝
• Std.Http.instReprVersion.repr Std.Http.Version.v11 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Version.v11")).group prec✝
• Std.Http.instReprVersion.repr Std.Http.Version.v20 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Version.v20")).group prec✝
• Std.Http.instReprVersion.repr Std.Http.Version.v30 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Version.v30")).group prec✝

@[implicit_reducible]

instance Std.Http.instReprVersion : Repr Version

Equations

• Std.Http.instReprVersion = { reprPrec := Std.Http.instReprVersion.repr }

def Std.Http.instInhabitedVersion.default : Version

Equations

• Std.Http.instInhabitedVersion.default = Std.Http.Version.v10

@[implicit_reducible]

instance Std.Http.instInhabitedVersion : Inhabited Version

Equations

• Std.Http.instInhabitedVersion = { default := Std.Http.instInhabitedVersion.default }

def Std.Http.instBEqVersion.beq : Version → Version → Bool

Equations

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

@[implicit_reducible]

instance Std.Http.instBEqVersion : BEq Version

Equations

• Std.Http.instBEqVersion = { beq := Std.Http.instBEqVersion.beq }

@[implicit_reducible]

instance Std.Http.instDecidableEqVersion : DecidableEq Version

Equations

• Std.Http.instDecidableEqVersion x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Std.Http.Version.ofNumber? : Nat → Nat → Option Version

Converts a pair of Nat to the corresponding Version.

Equations

• Std.Http.Version.ofNumber? 1 0 = some Std.Http.Version.v10
• Std.Http.Version.ofNumber? 1 1 = some Std.Http.Version.v11
• Std.Http.Version.ofNumber? 2 0 = some Std.Http.Version.v20
• Std.Http.Version.ofNumber? 3 0 = some Std.Http.Version.v30
• Std.Http.Version.ofNumber? x✝¹ x✝ = none

def Std.Http.Version.ofString? : String → Option Version

Converts String to the corresponding Version.

Equations

• Std.Http.Version.ofString? "HTTP/1.0" = some Std.Http.Version.v10
• Std.Http.Version.ofString? "HTTP/1.1" = some Std.Http.Version.v11
• Std.Http.Version.ofString? "HTTP/2.0" = some Std.Http.Version.v20
• Std.Http.Version.ofString? "HTTP/3.0" = some Std.Http.Version.v30
• Std.Http.Version.ofString? x✝ = none

def Std.Http.Version.ofString! (s : String) : Version

Converts String to the corresponding Version, panics if invalid.

Equations

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

def Std.Http.Version.toNumber : Version → Nat × Nat

Converts a Version to its corresponding major and minor numbers as a pair.

Equations

• Std.Http.Version.v10.toNumber = (1, 0)
• Std.Http.Version.v11.toNumber = (1, 1)
• Std.Http.Version.v20.toNumber = (2, 0)
• Std.Http.Version.v30.toNumber = (3, 0)

@[implicit_reducible]

instance Std.Http.Version.instToString : ToString Version

Equations

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