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

fix: bug in reference implementation of String.get?

Browse source
This commit is contained in:
Mario Carneiro 2023-05-12 18:07:11 -04:00 • committed by Leonardo de Moura
parent ad4b822734
commit 7f84bf07ba
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -60,7 +60,7 @@ def get (s : @& String) (p : @& Pos) : Char :=
def utf8GetAux? : List Char → Pos → Pos → Option Char
| [], _, _ => none
| c::cs, i, p => if i = p then c else utf8GetAux cs (i + c) p
| c::cs, i, p => if i = p then c else utf8GetAux? cs (i + c) p
@[extern "lean_string_utf8_get_opt"]
def get? : (@& String) → (@& Pos) → Option Char