From 7f84bf07ba094fde1fc49da40883a2cb30525c0c Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Fri, 12 May 2023 18:07:11 -0400
Subject: [PATCH] fix: bug in reference implementation of String.get?

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