From 367b38701fb9cca80328624a016c3b3acfd5e2cd Mon Sep 17 00:00:00 2001 From: Bulhwi Cha Date: Wed, 19 Jul 2023 20:50:27 +0900 Subject: [PATCH] refactor: simplify `String.splitOnAux` (#2271) --- src/Init/Data/String/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Data/String/Basic.lean b/src/Init/Data/String/Basic.lean index f28d56d9cf..12363c3111 100644 --- a/src/Init/Data/String/Basic.lean +++ b/src/Init/Data/String/Basic.lean @@ -247,7 +247,7 @@ termination_by _ => s.endPos.1 - i.1 def splitOnAux (s sep : String) (b : Pos) (i : Pos) (j : Pos) (r : List String) : List String := if h : s.atEnd i then - let r := if sep.atEnd j then ""::(s.extract b (i - j))::r else (s.extract b i)::r + let r := (s.extract b i)::r r.reverse else have := Nat.sub_lt_sub_left (Nat.gt_of_not_le (mt decide_eq_true h)) (lt_next s _)