sdgoij/lean4
1
0
Fork 0
mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 18:34:06 +00:00
Code Issues Packages Projects Releases Wiki Activity

refactor: head to line

Browse Source
This commit is contained in:
Sofia Rodrigues
2026-03-03 12:08:26 -03:00
parent bd4af50d04
commit 710eee2b49
2 changed files with 8 additions and 8 deletions
Download Patch File Download Diff File Expand all files Collapse all files

8
src/Std/Internal/Http/Data/Request.lean
View File

@@ -151,13 +151,13 @@ def uri (builder : Builder) (uri : String) : Builder :=
Sets the headers for the request being built.
-/
def headers (builder : Builder) (headers : Headers) : Builder :=
{ builder with head := { builder.head with headers } }
{ builder with line := { builder.line with headers } }
/--
Adds a single header to the request being built.
-/
def header (builder : Builder) (key : Header.Name) (value : Header.Value) : Builder :=
{ builder with head := { builder.head with headers := builder.head.headers.insert key value } }
{ builder with line := { builder.line with headers := builder.line.headers.insert key value } }
/--
Adds a single header to the request being built, panics if the header is invalid.
@@ -165,7 +165,7 @@ Adds a single header to the request being built, panics if the header is invalid
def header! (builder : Builder) (key : String) (value : String) : Builder :=
let key := Header.Name.ofString! key
let value := Header.Value.ofString! value
{ builder with head := { builder.head with headers := builder.head.headers.insert key value } }
{ builder with line := { builder.line with headers := builder.line.headers.insert key value } }
/--
Adds a single header to the request being built.
@@ -174,7 +174,7 @@ Returns `none` if the header name or value is invalid.
def header? (builder : Builder) (key : String) (value : String) : Option Builder := do
let key ← Header.Name.ofString? key
let value ← Header.Value.ofString? value
pure <| { builder with head := { builder.head with headers := builder.head.headers.insert key value } }
pure <| { builder with line := { builder.line with headers := builder.line.headers.insert key value } }
/--
Adds a header to the request being built only if the Option Header.Value is some.

8
src/Std/Internal/Http/Data/Response.lean
View File

@@ -123,13 +123,13 @@ def status (builder : Builder) (status : Status) : Builder :=
Sets the headers for the response being built.
-/
def headers (builder : Builder) (headers : Headers) : Builder :=
{ builder with head := { builder.head with headers } }
{ builder with line := { builder.line with headers } }
/--
Adds a single header to the response being built.
-/
def header (builder : Builder) (key : Header.Name) (value : Header.Value) : Builder :=
{ builder with head := { builder.head with headers := builder.head.headers.insert key value } }
{ builder with line := { builder.line with headers := builder.line.headers.insert key value } }
/--
Adds a single header to the response being built, panics if the header is invalid.
@@ -137,7 +137,7 @@ Adds a single header to the response being built, panics if the header is invali
def header! (builder : Builder) (key : String) (value : String) : Builder :=
let key := Header.Name.ofString! key
let value := Header.Value.ofString! value
{ builder with head := { builder.head with headers := builder.head.headers.insert key value } }
{ builder with line := { builder.line with headers := builder.line.headers.insert key value } }
/--
Adds a single header to the response being built.
@@ -146,7 +146,7 @@ Returns `none` if the header name or value is invalid.
def header? (builder : Builder) (key : String) (value : String) : Option Builder := do
let key ← Header.Name.ofString? key
let value ← Header.Value.ofString? value
pure <| { builder with head := { builder.head with headers := builder.head.headers.insert key value } }
pure <| { builder with line := { builder.line with headers := builder.line.headers.insert key value } }
/--
Inserts a typed extension value into the response being built.