Skip to content

Commit 1678d1e

Browse files
committed
Import
1 parent 761cbe8 commit 1678d1e

File tree

1 file changed

+1
-0
lines changed

1 file changed

+1
-0
lines changed

src/Init/Data/String/Lemmas.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ module
77

88
prelude
99
public import Init.Data.String.Lemmas.Splits
10+
public import Init.Data.String.Lemmas.Modify
1011
public import Init.Data.Char.Order
1112
public import Init.Data.Char.Lemmas
1213
public import Init.Data.List.Lex

0 commit comments

Comments
 (0)