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: move test from encode to the uri tests

Browse Source
This commit is contained in:
Sofia Rodrigues
2026-03-04 10:20:25 -03:00
parent 3dfb5e002a
commit 39ab2b289c
1 changed files with 3 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

3
tests/lean/run/async_http_uri.lean
View File

@@ -214,6 +214,7 @@ info: some " "
#eval parseCheck "http://user%40example:pass%3Aword@host.com"
#eval parseCheck "http://example.com:/"
#eval parseCheck "http://example.com:/?q=1"
#eval parseCheck "///////"
-- `&` in a key must be percent-encoded so toRawString round-trips correctly.
#guard
@@ -263,6 +264,8 @@ info: some " "
#eval parseCheckFail "#frag"
#eval parseCheckFail "/path/\n"
#eval parseCheckFail "/path/\u0000"
#eval parseCheckFail "/page#section"
#eval parseCheckFail "/api/v1/users/[id]:action"
-- maxPathSegments should apply to trailing empty segments as well.
#guard