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

style: change field names

Browse Source
This commit is contained in:
Sofia Rodrigues
2026-03-03 12:38:52 -03:00
parent 6189d4c130
commit 238925a681
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