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

fix: test

Browse Source
This commit is contained in:
Sofia Rodrigues
2026-03-13 23:54:45 -03:00
parent ae5a3d2c8b
commit 7fbecca6f0
1 changed files with 2 additions and 2 deletions
Download Patch File Download Diff File Expand all files Collapse all files

4
tests/elab/async_http_connection.lean
View File

@@ -406,7 +406,7 @@ def hasUri (req : Request Body.Incoming) (uri : String) : Bool :=
request :=
Request.new
|>.method .get
|>.uri (.originForm (.mk #[URI.EncodedString.encode <| String.ofList (List.replicate 2000 'a')] true) none)
|>.uri (.originForm ⟨(.mk #[URI.EncodedString.encode <| String.ofList (List.replicate 2000 'a')] true), none⟩)
|>.header! "Host" "api.example.com"
|>.header! "Connection" "close"
|>.body #[]
@@ -423,7 +423,7 @@ def hasUri (req : Request Body.Incoming) (uri : String) : Bool :=
request :=
Request.new
|>.method .get
|>.uri (.originForm (.mk #[URI.EncodedString.encode <| String.ofList (List.replicate 200 'a')] true) none)
|>.uri (.originForm ⟨(.mk #[URI.EncodedString.encode <| String.ofList (List.replicate 200 'a')] true), none⟩)
|>.header! "Host" (String.ofList (List.replicate 8230 'a'))
|>.header! "Connection" "close"
|>.body #[]