From fd72fdf8f84a56c5e906ece4ae43649d08cf52bd Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Wed, 17 May 2023 00:33:12 -0400
Subject: [PATCH] fix: incorrect utf8 in splitAux

---
 src/Init/Data/String/Basic.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Init/Data/String/Basic.lean b/src/Init/Data/String/Basic.lean
index ff56ef6a3a..4e9fe6791c 100644
--- a/src/Init/Data/String/Basic.lean
+++ b/src/Init/Data/String/Basic.lean
@@ -236,8 +236,8 @@ where
   else
     have := Nat.sub_lt_sub_left (Nat.gt_of_not_le (mt decide_eq_true h)) (lt_next s _)
     if p (s.get i) then
-      let i := s.next i
-      splitAux s p i i (s.extract b { byteIdx := i.byteIdx - 1 } :: r)
+      let i' := s.next i
+      splitAux s p i' i' (s.extract b i :: r)
     else
       splitAux s p b (s.next i) r
 termination_by _ => s.endPos.1 - i.1