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

Merge branch 'sofia/async-http-uri' into sofia/async-http-body

Browse Source
This commit is contained in:
Sofia Rodrigues
2026-03-12 15:39:08 -03:00
parent c0e60b797c 72244398dc
commit e359001026
1 changed files with 0 additions and 16 deletions
Download Patch File Download Diff File Expand all files Collapse all files

16
tests/elab/async_http_uri.lean
View File

@@ -302,14 +302,6 @@ info: Std.Http.RequestTarget.asteriskForm
let result ← runParser parseRequestTarget "*"
IO.println (repr result)
/--
info: none
-/
#guard_msgs in
#eval show IO _ from do
let result ← runParser parseRequestTarget "https://ata/b?ata=be"
IO.println (repr (result.fragment?))
/--
info: #[("q", some "hello%20world"), ("category", some "tech%2Bgames")]
-/
@@ -794,14 +786,6 @@ info: key=new
|>.set "key" "new"
IO.println query.toRawString
/--
info: none
-/
#guard_msgs in
#eval show IO _ from do
let result ← runParser parseRequestTarget "/path"
IO.println (repr result.fragment?)
-- ============================================================================
-- URI Builder Tests
-- ============================================================================