Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit d7283d7

Browse files
khoekmergify[bot]
authored andcommitted
feat(string): split_on a char (#1145)
* lib: string * type
1 parent a35d682 commit d7283d7

File tree

1 file changed

+4
-0
lines changed

1 file changed

+4
-0
lines changed

src/data/string/defs.lean

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
1+
import data.list.defs
12

23
namespace string
34

@@ -7,4 +8,7 @@ intercalate (singleton c) ∘ f ∘ split (= c)
78
def over_list (f : list char → list char) : string → string :=
89
list.as_string ∘ f ∘ string.to_list
910

11+
def split_on (c : char) (s : string) : list string :=
12+
(s.to_list.split_on c).map list.as_string
13+
1014
end string

0 commit comments

Comments
 (0)