diff --git a/tests/lean/string_imp2.lean b/tests/lean/string_imp2.lean
index 5ce398b938..80dff0c48d 100644
--- a/tests/lean/string_imp2.lean
+++ b/tests/lean/string_imp2.lean
@@ -58,3 +58,7 @@ def ssDots : Substring := "____abc.αβγ.123.____".toSubstring.extract ⟨4⟩
 #eval ssDots.splitOn "."
 def ssHyphs : Substring := "____abc--αβγ--123--____".toSubstring.extract ⟨4⟩ ⟨22⟩
 #eval ssHyphs.splitOn "--"
+
+#eval "αβγ".get' 0 (by decide)
+#eval "αβγ".get' ⟨2⟩ (by decide)
+#eval "αβγ".next' ⟨2⟩ (by decide)
diff --git a/tests/lean/string_imp2.lean.expected.out b/tests/lean/string_imp2.lean.expected.out
index 87c1751906..abc5396f34 100644
--- a/tests/lean/string_imp2.lean.expected.out
+++ b/tests/lean/string_imp2.lean.expected.out
@@ -42,3 +42,6 @@ false
 "abcd".toSubstring
 ["abc".toSubstring, "αβγ".toSubstring, "123".toSubstring, "".toSubstring]
 ["abc".toSubstring, "αβγ".toSubstring, "123".toSubstring, "".toSubstring]
+'α'
+'β'
+{ byteIdx := 4 }