Headers

This module defines the Headers type, which represents a collection of HTTP header name-value pairs.

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

structure Std.Http.Headers : Type

A structure for managing HTTP headers as key-value pairs.

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

• map : Internal.IndexMultiMap Header.Name Header.Value

  The underlying multimap that stores headers.

@[implicit_reducible]

instance Std.Http.instInhabitedHeaders : Inhabited Headers

def Std.Http.instInhabitedHeaders.default : Headers

@[implicit_reducible]

instance Std.Http.instReprHeaders : Repr Headers

def Std.Http.instReprHeaders.repr : Headers → Nat → Format

@[implicit_reducible]

instance Std.Http.instMembershipNameHeaders : Membership Header.Name Headers

@[implicit_reducible]

instance Std.Http.instDecidableMemNameHeaders (name : Header.Name) (h : Headers) : Decidable (name ∈ h)

@[inline]

def Std.Http.Headers.get (headers : Headers) (name : Header.Name) (h : name ∈ headers) : Header.Value

Retrieves the first Header.Value for the given key.

@[inline]

def Std.Http.Headers.getAll (headers : Headers) (name : Header.Name) (h : name ∈ headers) : Array Header.Value

Retrieves all Header.Value entries for the given key.

@[inline]

def Std.Http.Headers.getAll? (headers : Headers) (name : Header.Name) : Option (Array Header.Value)

Like getAll, but returns none instead of requiring a membership proof. Returns none if the header is absent.

@[inline]

def Std.Http.Headers.get? (headers : Headers) (name : Header.Name) : Option Header.Value

Retrieves the first Header.Value for the given key. Returns none if the header is absent.

@[inline]

def Std.Http.Headers.hasEntry (headers : Headers) (name : Header.Name) (value : Header.Value) : Bool

Checks if the entry is present in the Headers.

@[inline]

def Std.Http.Headers.getLast? (headers : Headers) (name : Header.Name) : Option Header.Value

Retrieves the last header value for the given key. Returns none if the header is absent.

@[inline]

def Std.Http.Headers.getD (headers : Headers) (name : Header.Name) (d : Header.Value) : Header.Value

Like get?, but returns a default value if absent.

@[inline]

def Std.Http.Headers.get! (headers : Headers) (name : Header.Name) : Header.Value

Like get?, but panics if absent.

@[inline]

def Std.Http.Headers.insert (headers : Headers) (key : Header.Name) (value : Header.Value) : Headers

Inserts a new key-value pair into the headers.

@[inline]

def Std.Http.Headers.insert! (headers : Headers) (name value : String) : Headers

Adds a header from string name and value, panicking if either is invalid.

@[inline]

def Std.Http.Headers.insert? (headers : Headers) (name value : String) : Option Headers

Adds a header from string name and value. Returns none if either the header name or value is invalid.

@[inline]

def Std.Http.Headers.insertMany (headers : Headers) (key : Header.Name) (values : Array Header.Value) : Headers

Inserts a new key with an array of values.

def Std.Http.Headers.empty : Headers

Creates empty headers.

def Std.Http.Headers.ofList (pairs : List (Header.Name × Header.Value)) : Headers

Creates headers from a list of key-value pairs.

@[inline]

def Std.Http.Headers.contains (headers : Headers) (name : Header.Name) : Bool

Checks if a header with the given name exists.

@[inline]

def Std.Http.Headers.erase (headers : Headers) (name : Header.Name) : Headers

Removes a header with the given name.

@[inline]

def Std.Http.Headers.size (headers : Headers) : Nat

Gets the number of headers.

@[inline]

def Std.Http.Headers.isEmpty (headers : Headers) : Bool

Checks if the headers are empty.

def Std.Http.Headers.merge (headers1 headers2 : Headers) : Headers

Merges two headers, accumulating values for duplicate keys from both.

def Std.Http.Headers.toList (headers : Headers) : List (Header.Name × Header.Value)

Converts the headers to a list of key-value pairs (flattened). Each header with multiple values produces multiple pairs.

def Std.Http.Headers.toArray (headers : Headers) : Array (Header.Name × Header.Value)

Converts the headers to an array of key-value pairs (flattened). Each header with multiple values produces multiple pairs.

def Std.Http.Headers.fold {α : Type u_1} (headers : Headers) (init : α) (f : α → Header.Name → Header.Value → α) : α

Folds over all key-value pairs in the headers.

def Std.Http.Headers.mapValues (headers : Headers) (f : Header.Name → Header.Value → Header.Value) : Headers

Maps a function over all header values, producing new headers.

def Std.Http.Headers.filterMap (headers : Headers) (f : Header.Name → Header.Value → Option Header.Value) : Headers

Filters and maps over header key-value pairs. Returns only the pairs for which the function returns some.

def Std.Http.Headers.filter (headers : Headers) (f : Header.Name → Header.Value → Bool) : Headers

Filters header key-value pairs, keeping only those that satisfy the predicate.

def Std.Http.Headers.update (headers : Headers) (name : Header.Name) (f : Header.Value → Header.Value) : Headers

Updates all the values of a header if it exists.

@[inline]

def Std.Http.Headers.replaceLast (headers : Headers) (name : Header.Name) (value : Header.Value) : Headers

Replaces the last value for the given header name. If the header is absent, returns the headers unchanged.

@[implicit_reducible]

instance Std.Http.Headers.instToString : ToString Headers

@[implicit_reducible]

instance Std.Http.Headers.instEncodeV11 : Internal.Encode Version.v11 Headers

@[implicit_reducible]

instance Std.Http.Headers.instEmptyCollection : EmptyCollection Headers

@[implicit_reducible]

instance Std.Http.Headers.instSingletonProdNameValue : Singleton (Header.Name × Header.Value) Headers

@[implicit_reducible]

instance Std.Http.Headers.instInsertProdNameValue : Insert (Header.Name × Header.Value) Headers

@[implicit_reducible]

instance Std.Http.Headers.instUnion : Union Headers

@[implicit_reducible]

instance Std.Http.Headers.instForInProdNameValueOfMonad {m : Type u_1 → Type u_2} [Monad m] : ForIn m Headers (Header.Name × Header.Value)