summaryrefslogtreecommitdiff
path: root/Common/String.lean
diff options
context:
space:
mode:
Diffstat (limited to 'Common/String.lean')
-rw-r--r--Common/String.lean2
1 files changed, 1 insertions, 1 deletions
diff --git a/Common/String.lean b/Common/String.lean
index 3edbd63..955affe 100644
--- a/Common/String.lean
+++ b/Common/String.lean
@@ -1,6 +1,6 @@
namespace String
def splitTrim (c : Char → Bool) (s : String) : List String :=
- String.trim <$> s.split c
+ String.trim <$> s.splitToList c
def notEmpty : String → Bool := not ∘ isEmpty