Extensions

This module provides the Extensions type, a dynamically-typed map for storing metadata on HTTP requests and responses. It can be used by parsers, middleware, or other processing stages to attach arbitrary typed data.

def Std.Http.Extensions.compareName : Lean.Name → Lean.Name → Ordering

An ordering for Name keys used by Extensions.

structure Std.Http.Extensions : Type

A dynamically typed map for optional metadata that can be attached to HTTP requests and responses. Extensions allow storing arbitrary typed data keyed by type name, useful for metadata such as socket information or custom processing data.

• data : Std.TreeMap Lean.Name Dynamic Std.Http.Extensions.compareName

@[implicit_reducible]

instance Std.Http.instInhabitedExtensions : Inhabited Extensions

def Std.Http.instInhabitedExtensions.default : Extensions

def Std.Http.Extensions.empty : Extensions

An empty extensions map with no data.

@[inline]

def Std.Http.Extensions.get (x : Extensions) (α : Type) [TypeName α] : Option α

Retrieves a value of type α from the extensions, if present.

@[inline]

def Std.Http.Extensions.insert {α : Type u_1} (x : Extensions) [TypeName α] (data : α) : Extensions

Inserts a value into the extensions, keyed by its type name. If a value of the same type already exists, it is replaced.

@[inline]

def Std.Http.Extensions.remove (x : Extensions) (α : Type) [TypeName α] : Extensions

Removes the value of type α from the extensions.

@[inline]

def Std.Http.Extensions.contains (x : Extensions) (α : Type) [TypeName α] : Bool

Checks whether the extensions contain a value of type α.