Skip to content

Commit 4e9af59

Browse files
committed
fix: domain name comment
1 parent 0c645c8 commit 4e9af59

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/Std/Internal/Http/Data/URI/Basic.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -55,7 +55,7 @@ structure UserInfo where
5555
deriving Inhabited, Repr
5656

5757
/--
58-
?
58+
A domain name represented as a lowercase-normalized string.
5959
-/
6060
abbrev DomainName := { s : String // IsLowerCase s }
6161

0 commit comments

Comments
 (0)