structure Network.HTTP.Date.HTTPDate : Type

An HTTP date with bounded fields. $$\text{HTTPDate} = \{ y : \mathbb{N},\; m : [1,12],\; d : [1,31],\; h : [0,23],\; \min : [0,59],\; s : [0,60] \}$$ (seconds up to 60 for leap seconds)

• year : Nat
• month : Nat
• day : Nat
• hour : Nat
• minute : Nat
• second : Nat

@[implicit_reducible]

instance Network.HTTP.Date.instBEqHTTPDate : BEq HTTPDate

Equations

• Network.HTTP.Date.instBEqHTTPDate = { beq := Network.HTTP.Date.instBEqHTTPDate.beq }

def Network.HTTP.Date.instBEqHTTPDate.beq : HTTPDate → HTTPDate → Bool

Equations

• One or more equations did not get rendered due to their size.
• Network.HTTP.Date.instBEqHTTPDate.beq x✝¹ x✝ = false

def Network.HTTP.Date.instReprHTTPDate.repr : HTTPDate → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Network.HTTP.Date.instReprHTTPDate : Repr HTTPDate

Equations

• Network.HTTP.Date.instReprHTTPDate = { reprPrec := Network.HTTP.Date.instReprHTTPDate.repr }

@[implicit_reducible]

instance Network.HTTP.Date.instToStringHTTPDate : ToString HTTPDate

Equations

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

def Network.HTTP.Date.HTTPDate.parseHTTPDate (s : String) : Option HTTPDate

Parse an HTTP date string. Supports IMF-fixdate and asctime formats. $$\text{parseHTTPDate} : \text{String} \to \text{Option}(\text{HTTPDate})$$

Equations

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

def Network.HTTP.Date.HTTPDate.formatHTTPDate (d : HTTPDate) : String

Format an HTTP date in IMF-fixdate format (RFC 7231 preferred). $$\text{formatHTTPDate} : \text{HTTPDate} \to \text{String}$$ Note: day-of-week is computed from the date.

Equations

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