feat: introduce Headers data type for HTTP

src/Init/Data/String/Defs.lean

@@ -230,7 +230,7 @@ Examples:
  * `"empty".isEmpty = false`
  * `" ".isEmpty = false`
 -/
-@[inline] def isEmpty (s : String) : Bool :=
+@[inline, expose] def isEmpty (s : String) : Bool :=
   s.utf8ByteSize == 0
 
 @[export lean_string_isempty]

src/Init/Data/String/Lemmas/Modify.lean

@@ -57,4 +57,14 @@ theorem length_map {f : Char → Char} {s : String} : (s.map f).length = s.lengt
 theorem map_eq_empty {f : Char → Char} {s : String} : s.map f = "" ↔ s = "" := by
   simp [← toList_eq_nil_iff]
 
+@[simp]
+theorem map_map {f g : Char → Char} {s : String} : String.map g (String.map f s) = String.map (g ∘ f) s  := by
+  apply String.ext
+  simp [List.map_map]
+
+@[simp]
+theorem map_id {s : String} : String.map id s = s := by
+  apply String.ext
+  simp [List.map_id]
+
 end String

src/Init/Data/String/Modify.lean

@@ -229,7 +229,7 @@ Examples:
 * `"Orange".toLower = "orange"`
 * `"ABc123".toLower = "abc123"`
 -/
-@[inline] def toLower (s : String) : String :=
+@[inline, expose] def toLower (s : String) : String :=
   s.map Char.toLower
 
 /--

src/Std/Internal/Http/Data.lean

@@ -12,6 +12,7 @@ public import Std.Internal.Http.Data.Request
 public import Std.Internal.Http.Data.Response
 public import Std.Internal.Http.Data.Status
 public import Std.Internal.Http.Data.Chunk
+public import Std.Internal.Http.Data.Headers
 
 /-!
 # HTTP Data Types

src/Std/Internal/Http/Data/Chunk.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Std.Internal.Http.Internal
+public import Std.Internal.Http.Data.Headers
 public meta import Std.Internal.Http.Internal.String
 
 public section
@@ -20,8 +21,7 @@ Reference: https://www.rfc-editor.org/rfc/rfc9112.html#section-7.1
 -/
 
 namespace Std.Http
-
-open Internal
+open Internal Char
 
 set_option linter.all true
 
@@ -208,3 +208,114 @@ instance : Encode .v11 Chunk where
     buffer.append #[size, exts.toUTF8, "\r\n".toUTF8, chunk.data, "\r\n".toUTF8]
 
 end Chunk
+
+
+/--
+Trailer headers sent after the final chunk in HTTP/1.1 chunked transfer encoding.
+Per RFC 9112 §7.1.2, trailers allow the sender to include additional metadata after
+the message body, such as message integrity checks or digital signatures.
+-/
+structure Trailer where
+  /--
+  The trailer header fields as key-value pairs.
+  -/
+  headers : Headers
+deriving Inhabited
+
+namespace Trailer
+
+/--
+Creates an empty trailer with no headers.
+-/
+def empty : Trailer :=
+  { headers := .empty }
+
+/--
+Inserts a trailer header field.
+-/
+@[inline]
+def insert (trailer : Trailer) (name : Header.Name) (value : Header.Value) : Trailer :=
+  { headers := trailer.headers.insert name value }
+
+/--
+Inserts a trailer header field from string name and value, panicking if either is invalid.
+-/
+@[inline]
+def insert! (trailer : Trailer) (name : String) (value : String) : Trailer :=
+  { headers := trailer.headers.insert! name value }
+
+/--
+Retrieves the first value for the given trailer header name.
+Returns `none` if absent.
+-/
+@[inline]
+def get? (trailer : Trailer) (name : Header.Name) : Option Header.Value :=
+  trailer.headers.get? name
+
+/--
+Retrieves all values for the given trailer header name.
+Returns `none` if absent.
+-/
+@[inline]
+def getAll? (trailer : Trailer) (name : Header.Name) : Option (Array Header.Value) :=
+  trailer.headers.getAll? name
+
+/--
+Checks if a trailer header with the given name exists.
+-/
+@[inline]
+def contains (trailer : Trailer) (name : Header.Name) : Bool :=
+  trailer.headers.contains name
+
+/--
+Removes a trailer header with the given name.
+-/
+@[inline]
+def erase (trailer : Trailer) (name : Header.Name) : Trailer :=
+  { headers := trailer.headers.erase name }
+
+/--
+Gets the number of trailer headers.
+-/
+@[inline]
+def size (trailer : Trailer) : Nat :=
+  trailer.headers.size
+
+/--
+Checks if the trailer has no headers.
+-/
+@[inline]
+def isEmpty (trailer : Trailer) : Bool :=
+  trailer.headers.isEmpty
+
+/--
+Merges two trailers, accumulating values for duplicate keys from both.
+-/
+def merge (t1 t2 : Trailer) : Trailer :=
+  { headers := t1.headers.merge t2.headers }
+
+/--
+Converts the trailer headers to a list of key-value pairs.
+-/
+def toList (trailer : Trailer) : List (Header.Name × Header.Value) :=
+  trailer.headers.toList
+
+/--
+Converts the trailer headers to an array of key-value pairs.
+-/
+def toArray (trailer : Trailer) : Array (Header.Name × Header.Value) :=
+  trailer.headers.toArray
+
+/--
+Folds over all key-value pairs in the trailer headers.
+-/
+def fold (trailer : Trailer) (init : α) (f : α → Header.Name → Header.Value → α) : α :=
+  trailer.headers.fold init f
+
+instance : Encode .v11 Trailer where
+  encode buffer trailer :=
+    buffer.write "0\r\n".toUTF8
+    |> (Encode.encode .v11 · trailer.headers)
+    |>.write  "\r\n".toUTF8
+
+end Trailer