max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

test: String.get' and String.next'

Browse source
This commit is contained in:
Leonardo de Moura 2022-11-09 17:02:49 -08:00
parent afa567fc09
commit 7b8ade5ee4
2 changed files with 7 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
tests/lean/string_imp2.lean
View file

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

3
tests/lean/string_imp2.lean.expected.out
View file

@ -42,3 +42,6 @@ false
"abcd".toSubstring
["abc".toSubstring, "αβγ".toSubstring, "123".toSubstring, "".toSubstring]
["abc".toSubstring, "αβγ".toSubstring, "123".toSubstring, "".toSubstring]
'α'
'β'
{ byteIdx := 4 }