max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: incorrect utf8 in splitAux

Browse source
This commit is contained in:
Mario Carneiro 2023-05-17 00:33:12 -04:00 • committed by Leonardo de Moura
parent aa60791db3
commit fd72fdf8f8
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Init/Data/String/Basic.lean
View file

@ -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