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.

Equations

• Std.Http.Extensions.compareName Lean.Name.anonymous Lean.Name.anonymous = Ordering.eq
• Std.Http.Extensions.compareName Lean.Name.anonymous x✝ = Ordering.lt
• Std.Http.Extensions.compareName x✝ Lean.Name.anonymous = Ordering.gt
• Std.Http.Extensions.compareName (p₁.str s₁) (p₂.str s₂) = match Std.Http.Extensions.compareName p₁ p₂ with | Ordering.eq => compareOfLessAndEq s₁ s₂ | ord => ord
• Std.Http.Extensions.compareName (pre.str str) (pre_1.num i) = Ordering.lt
• Std.Http.Extensions.compareName (pre.num i) (pre_1.str str) = Ordering.gt
• Std.Http.Extensions.compareName (p₁.num n₁) (p₂.num n₂) = match Std.Http.Extensions.compareName p₁ p₂ with | Ordering.eq => compare n₁ n₂ | ord => ord

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

Equations

• Std.Http.instInhabitedExtensions = { default := Std.Http.instInhabitedExtensions.default }

def Std.Http.instInhabitedExtensions.default : Extensions

Equations

• Std.Http.instInhabitedExtensions.default = { data := default }

def Std.Http.Extensions.empty : Extensions

An empty extensions map with no data.

Equations

• Std.Http.Extensions.empty = { }

@[inline]

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

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

Equations

• x.get α = do let dyn ← (Std.Http.Extensions.data✝ x).get? (TypeName.typeName α) Dynamic.get? α dyn

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

Equations

• x.insert data = { data := (Std.Http.Extensions.data✝ x).insert (Dynamic.mk data).typeName (Dynamic.mk data) }

@[inline]

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

Removes the value of type α from the extensions.

Equations

• x.remove α = { data := (Std.Http.Extensions.data✝ x).erase (TypeName.typeName α) }

@[inline]

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

Checks whether the extensions contain a value of type α.

Equations

• x.contains α = (Std.Http.Extensions.data✝ x).contains (TypeName.typeName α)