Skip to content

Commit 8b58da0

Browse files
committed
fix: imports
1 parent 6649fc9 commit 8b58da0

File tree

2 files changed

+2
-2
lines changed

2 files changed

+2
-2
lines changed

src/Std/Internal/Http/Data/Method.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ Authors: Sofia Rodrigues
66
module
77

88
prelude
9-
public import Init.Data
9+
public import Init.Data.Repr
1010
public import Std.Internal.Http.Encode
1111

1212
public section

src/Std/Internal/Http/Data/Version.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ Authors: Sofia Rodrigues
66
module
77

88
prelude
9-
public import Init
9+
public import Init.Data.String
1010

1111
public section
1212

0 commit comments

Comments
 (0)