diff --git a/src/Init/Data/String/Basic.lean b/src/Init/Data/String/Basic.lean index 08a18d9c4c..05818c777e 100644 --- a/src/Init/Data/String/Basic.lean +++ b/src/Init/Data/String/Basic.lean @@ -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