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: uri test

Browse Source
This commit is contained in:
Sofia Rodrigues
2026-03-13 23:46:35 -03:00
parent 3a4a309aed
commit d71f0bdae7
2 changed files with 3 additions and 3 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
src/Std/Internal/Http/Data/URI.lean
View File

@@ -50,7 +50,7 @@ The path should start with '/' (e.g., "/api/users" or "/search?q=test").
Panics if the string is not a valid origin-form request target.
-/
@[inline]
def pathAndQuery! (path : String) : RequestTarget :=
def originForm! (path : String) : RequestTarget :=
match parse? path with
| some (.originForm o) => .originForm o
| _ => panic! s!"invalid origin-form request target: {path}"

4
tests/elab/async_http_uri.lean
View File

@@ -586,9 +586,9 @@ info: /x/y
-- ============================================================================
#guard (URI.parse! "http://example.com").path.isEmpty = true
#guard (URI.parse! "http://example.com/").path.absoluteForm = true
#guard (URI.parse! "http://example.com/").path.absolute = true
#guard (URI.parse! "http://example.com/a").path.isEmpty = false
#guard (URI.parse! "http://example.com/a").path.absoluteForm = true
#guard (URI.parse! "http://example.com/a").path.absolute = true
-- ============================================================================
-- URI Modification Helpers