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-headers' into sofia/async-http-uri

Browse Source
This commit is contained in:
Sofia Rodrigues
2026-03-03 12:42:23 -03:00
parent 8cb236e9eb 238925a681
commit cfa5cf76fc
2 changed files with 5 additions and 5 deletions
Download Patch File Download Diff File Expand all files Collapse all files

8
src/Std/Internal/Http/Data/Headers/Name.lean
View File

@@ -49,14 +49,14 @@ structure Name where
value : String
/--
The proof that it's a valid header name
The proof that it's a valid header name.
-/
validHeaderName : IsValidHeaderName value := by decide
isValidHeaderValue : IsValidHeaderName value := by decide
/--
The proof that we stored the header name in normal form
The proof that we stored the header name in stored as a lower case string.
-/
normalForm : IsLowerCase value := by decide
isLowerCase : IsLowerCase value := by decide
deriving Repr, DecidableEq
namespace Name

2
src/Std/Internal/Http/Data/Headers/Value.lean
View File

@@ -55,7 +55,7 @@ structure Value where
/--
The proof that it's a valid header value.
-/
validHeaderValue : IsValidHeaderValue value := by decide
isValidHeaderValue : IsValidHeaderValue value := by decide
deriving BEq, DecidableEq, Repr
instance : Hashable Value where