Skip to content

Commit ad7fa87

Browse files
committed
fix: domain name comment
1 parent dbfe4e9 commit ad7fa87

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)