Header Values

This module defines the Value type, which represents validated HTTP header values that conform to HTTP standards.

Reference: https://www.rfc-editor.org/rfc/rfc9110.html#name-field-values

@[reducible, inline]

abbrev Std.Http.Header.IsValidHeaderValue (s : String) : Prop

Proposition that asserts all characters in a string are valid for HTTP header values, and that the first and last characters (if present) are field-vchar (not SP/HTAB).

field-value = field-content field-content = field-vchar [ 1( SP / HTAB / field-vchar ) field-vchar ]

Reference: https://www.rfc-editor.org/rfc/rfc9110.html#section-5.5

Equations

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

structure Std.Http.Header.Value : Type

A validated HTTP header value that ensures all characters conform to HTTP standards.

• value : String

  The string data.

• isValidHeaderValue : IsValidHeaderValue self.value

  The proof that it's a valid header value.

def Std.Http.Header.instBEqValue.beq : Value → Value → Bool

Equations

• One or more equations did not get rendered due to their size.
• Std.Http.Header.instBEqValue.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Std.Http.Header.instBEqValue : BEq Value

Equations

• Std.Http.Header.instBEqValue = { beq := Std.Http.Header.instBEqValue.beq }

def Std.Http.Header.instDecidableEqValue.decEq (x✝ x✝¹ : Value) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Std.Http.Header.instDecidableEqValue : DecidableEq Value

Equations

• Std.Http.Header.instDecidableEqValue = Std.Http.Header.instDecidableEqValue.decEq

def Std.Http.Header.instReprValue.repr : Value → Nat → Format

Equations

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

@[implicit_reducible]

instance Std.Http.Header.instReprValue : Repr Value

Equations

• Std.Http.Header.instReprValue = { reprPrec := Std.Http.Header.instReprValue.repr }

@[implicit_reducible]

instance Std.Http.Header.instHashableValue : Hashable Value

Equations

• Std.Http.Header.instHashableValue = { hash := hash ∘ Std.Http.Header.Value.value }

@[implicit_reducible]

instance Std.Http.Header.instInhabitedValue : Inhabited Value

Equations

• Std.Http.Header.instInhabitedValue = { default := { value := "", isValidHeaderValue := Std.Http.Header.instInhabitedValue._proof_1 } }

def Std.Http.Header.Value.ofString? (s : String) : Option Value

Attempts to create a Value from a String, returning none if the string contains invalid characters for HTTP header values.

Equations

• Std.Http.Header.Value.ofString? s = if h : Std.Http.Header.IsValidHeaderValue s.trimAscii.toString then some { value := s.trimAscii.toString, isValidHeaderValue := h } else none

def Std.Http.Header.Value.ofString! (s : String) : Value

Creates a Value from a string, panicking with an error message if the string contains invalid characters for HTTP header values.

Equations

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

def Std.Http.Header.Value.is (s : Value) (h : String) : Bool

Performs a case-insensitive comparison between a Value and a String. Returns true if they match.

Equations

• s.is h = (s.value.toLower == h.toLower)

@[implicit_reducible]

instance Std.Http.Header.Value.instToString : ToString Value

Equations

• Std.Http.Header.Value.instToString = { toString := fun (v : Std.Http.Header.Value) => v.value }