Skip to content

Commit edb6446

Browse files
committed
Adaptations
1 parent 2a2c59c commit edb6446

File tree

4 files changed

+3
-3
lines changed

4 files changed

+3
-3
lines changed

src/Init/Data/String.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -23,3 +23,4 @@ public import Init.Data.String.TakeDrop
2323
public import Init.Data.String.Modify
2424
public import Init.Data.String.Termination
2525
public import Init.Data.String.ToSlice
26+
public import Init.Data.String.Search

src/Lean/Compiler/FFI.lean

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

88
prelude
99
public import Init.System.FilePath
10-
import Init.Data.String.Modify
10+
import Init.Data.String.Search
1111

1212
public section
1313

src/Lean/Data/Lsp/Utf16.lean

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,6 @@ Authors: Marc Huisinga, Wojciech Nawrocki
77
module
88

99
prelude
10-
public import Init.Data.String
1110
public import Lean.Data.Lsp.BasicAux
1211
public import Lean.DeclarationRange
1312

src/Lean/DocString/Markdown.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ import Init.Data.Ord
1212
public import Lean.DocString.Types
1313
public import Init.Data.String.TakeDrop
1414
import Init.Data.String.Iterator
15-
public import Init.Data.String.Modify
15+
public import Init.Data.String.Search
1616

1717
set_option linter.missingDocs true
1818

0 commit comments

Comments
 (0)