From bbe6bd4e72d6a5e510cbbcf8839871b317c01e9c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 14 Mar 2022 15:42:58 -0700
Subject: [PATCH] chore: simplify `String.utf8ByteSize` reference
 implementation

---
 src/Init/Prelude.lean | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index 7e80115aba..eabd4c2fcd 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -1151,13 +1151,13 @@ instance : Inhabited Substring where
 def String.csize (c : Char) : Nat :=
   c.utf8Size.toNat
 
-private def String.utf8ByteSizeAux : List Char → Nat → Nat
-  | List.nil,       r => r
-  | List.cons c cs, r => utf8ByteSizeAux cs (hAdd r (csize c))
-
 @[extern "lean_string_utf8_byte_size"]
 def String.utf8ByteSize : (@& String) → Nat
-  | ⟨s⟩ => utf8ByteSizeAux s 0
+  | ⟨s⟩ => go s
+where
+  go : List Char → Nat
+   | .nil       => 0
+   | .cons c cs => hAdd (go cs) (csize c)
 
 @[inline] def String.bsize (s : String) : Nat :=
   utf8ByteSize s