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

test: rename head to line

Browse Source
This commit is contained in:
Sofia Rodrigues
2026-03-03 12:43:44 -03:00
parent f14977f495
commit 53c9277209
1 changed files with 10 additions and 10 deletions
Download Patch File Download Diff File Expand all files Collapse all files

20
tests/lean/run/async_http_body.lean
View File

@@ -331,8 +331,8 @@ def requestBuilderText : Async Unit := do
let req ← Request.post (.originForm! "/api")
|>.text "Hello, World!"
assert! req.head.headers.get? Header.Name.contentType == some (Header.Value.ofString! "text/plain; charset=utf-8")
assert! req.head.headers.get? Header.Name.contentLength == none
assert! req.line.headers.get? Header.Name.contentType == some (Header.Value.ofString! "text/plain; charset=utf-8")
assert! req.line.headers.get? Header.Name.contentLength == none
let body ← recvBuiltBody req.body
assert! body.isSome
@@ -346,8 +346,8 @@ def requestBuilderJson : Async Unit := do
let req ← Request.post (.originForm! "/api")
|>.json "{\"key\": \"value\"}"
assert! req.head.headers.get? Header.Name.contentType == some (Header.Value.ofString! "application/json")
assert! req.head.headers.get? Header.Name.contentLength == none
assert! req.line.headers.get? Header.Name.contentType == some (Header.Value.ofString! "application/json")
assert! req.line.headers.get? Header.Name.contentLength == none
let body ← recvBuiltBody req.body
assert! body.isSome
assert! body.get!.data == "{\"key\": \"value\"}".toUTF8
@@ -361,7 +361,7 @@ def requestBuilderFromBytes : Async Unit := do
let req ← Request.post (.originForm! "/api")
|>.fromBytes data
assert! req.head.headers.get? Header.Name.contentLength == none
assert! req.line.headers.get? Header.Name.contentLength == none
let body ← recvBuiltBody req.body
assert! body.isSome
assert! body.get!.data == data
@@ -386,8 +386,8 @@ def responseBuilderText : Async Unit := do
let res ← Response.ok
|>.text "Hello, World!"
assert! res.head.headers.get? Header.Name.contentType == some (Header.Value.ofString! "text/plain; charset=utf-8")
assert! res.head.headers.get? Header.Name.contentLength == none
assert! res.line.headers.get? Header.Name.contentType == some (Header.Value.ofString! "text/plain; charset=utf-8")
assert! res.line.headers.get? Header.Name.contentLength == none
let body ← recvBuiltBody res.body
assert! body.isSome
@@ -401,8 +401,8 @@ def responseBuilderJson : Async Unit := do
let res ← Response.ok
|>.json "{\"status\": \"ok\"}"
assert! res.head.headers.get? Header.Name.contentType == some (Header.Value.ofString! "application/json")
assert! res.head.headers.get? Header.Name.contentLength == none
assert! res.line.headers.get? Header.Name.contentType == some (Header.Value.ofString! "application/json")
assert! res.line.headers.get? Header.Name.contentLength == none
let body ← recvBuiltBody res.body
assert! body.isSome
assert! body.get!.data == "{\"status\": \"ok\"}".toUTF8
@@ -416,7 +416,7 @@ def responseBuilderFromBytes : Async Unit := do
let res ← Response.ok
|>.fromBytes data
assert! res.head.headers.get? Header.Name.contentLength == none
assert! res.line.headers.get? Header.Name.contentLength == none
let body ← recvBuiltBody res.body
assert! body.isSome
assert! body.get!.data == data