Header Names

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

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

@[reducible, inline]

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

Proposition asserting that a string is a valid HTTP header name: all characters are valid token characters and the string is non-empty.

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

structure Std.Http.Header.Name : Type

A validated HTTP header name that ensures all characters conform to HTTP standards. Header names are case-insensitive according to HTTP specifications.

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

• value : String

  The lowercased normalized header name string.

• isValidHeaderValue : IsValidHeaderName self.value

  The proof that it's a valid header name.

• isLowerCase : Internal.IsLowerCase self.value

  The proof that we stored the header name in stored as a lower case string.

theorem Std.Http.Header.Name.ext {x y : Name} (value : x.value = y.value) : x = y

theorem Std.Http.Header.Name.ext_iff {x y : Name} : x = y ↔ x.value = y.value

@[implicit_reducible]

instance Std.Http.Header.instReprName : Repr Name

def Std.Http.Header.instReprName.repr : Name → Nat → Format

@[implicit_reducible]

instance Std.Http.Header.instDecidableEqName : DecidableEq Name

def Std.Http.Header.instDecidableEqName.decEq (x✝ x✝¹ : Name) : Decidable (x✝ = x✝¹)

@[implicit_reducible]

instance Std.Http.Header.Name.instBEq : BEq Name

@[implicit_reducible]

instance Std.Http.Header.Name.instHashable : Hashable Name

theorem Std.Http.Header.Name.Name.beq_eq {x y : Name} : (x == y) = (x.value == y.value)

instance Std.Http.Header.Name.instLawfulBEq : LawfulBEq Name

instance Std.Http.Header.Name.instLawfulHashable : LawfulHashable Name

@[implicit_reducible]

instance Std.Http.Header.Name.instInhabited : Inhabited Name

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

Attempts to create a Name from a String, returning none if the string contains invalid characters for HTTP header names or is empty.

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

Creates a Name from a string, panicking with an error message if the string contains invalid characters for HTTP header names or is empty.

@[inline]

def Std.Http.Header.Name.toCanonical (name : Name) : String

Converts the header name to title case (e.g., "Content-Type").

Note: some well-known headers have unconventional casing (e.g., "WWW-Authenticate"), but since HTTP header names are case-insensitive, this always uses simple capitalization.

def Std.Http.Header.Name.is (name : Name) (s : String) : Bool

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

@[implicit_reducible]

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

def Std.Http.Header.Name.contentType : Name

Standard Content-Type header name

def Std.Http.Header.Name.contentLength : Name

Standard Content-Length header name

def Std.Http.Header.Name.host : Name

Standard Host header name

def Std.Http.Header.Name.authorization : Name

Standard Authorization header name

def Std.Http.Header.Name.userAgent : Name

Standard User-Agent header name

def Std.Http.Header.Name.accept : Name

Standard Accept header name

def Std.Http.Header.Name.connection : Name

Standard Connection header name

def Std.Http.Header.Name.transferEncoding : Name

Standard Transfer-Encoding header name

def Std.Http.Header.Name.server : Name

Standard Server header name

def Std.Http.Header.Name.date : Name

Standard Date header name

def Std.Http.Header.Name.expect : Name

Standard Expect header name