@[reducible, inline]

abbrev Network.Wai.Handler.Warp.HeaderMap : Type

A specialized hash map for string keys. Uses Lean's standard HashMap.

Equations

• Network.Wai.Handler.Warp.HeaderMap = Std.HashMap String String

@[inline]

def Network.Wai.Handler.Warp.HeaderMap.empty : HeaderMap

Create an empty header map.

Equations

• Network.Wai.Handler.Warp.HeaderMap.empty = ∅

@[inline]

def Network.Wai.Handler.Warp.HeaderMap.insert' (m : HeaderMap) (k v : String) : HeaderMap

Insert a key-value pair.

Equations

• m.insert' k v = Std.HashMap.insert m k v

@[inline]

def Network.Wai.Handler.Warp.HeaderMap.find? (m : HeaderMap) (k : String) : Option String

Look up a value by key.

Equations

• m.find? k = Std.HashMap.get? m k