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.

@[instance_reducible]

instance Std.Http.instInhabitedHeaders : Inhabited Headers

@[instance_reducible]

instance Std.Http.instReprHeaders : Repr Headers

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

@[instance_reducible]

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

@[instance_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.eraseMany (headers : Headers) (names : Array Header.Name) : Headers

Removes all headers whose names appear in names. Names not present are ignored. Cheaper than chaining erase calls because IndexMultiMap.eraseMany rebuilds the index once in total rather than once per erase call.

@[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.

@[instance_reducible]

instance Std.Http.Headers.instToString : ToString Headers

@[instance_reducible]

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

@[instance_reducible]

instance Std.Http.Headers.instEmptyCollection : EmptyCollection Headers

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

instance Std.Http.Headers.instUnion : Union Headers

@[instance_reducible]

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