From 7b8ade5ee485e8ad2d7aad7107b2ffd4b2a7d69e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 9 Nov 2022 17:02:49 -0800
Subject: [PATCH] test: `String.get'` and `String.next'`

---
 tests/lean/string_imp2.lean              | 4 ++++
 tests/lean/string_imp2.lean.expected.out | 3 +++
 2 files changed, 7 insertions(+)

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 }