Skip to content

Commit 7dc88f0

Browse files
committed
more tests
1 parent c45f2af commit 7dc88f0

File tree

2 files changed

+4
-1
lines changed

2 files changed

+4
-1
lines changed

src/Init/Data/String/Pattern/String.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -129,7 +129,7 @@ instance (s : Slice) : Std.Iterators.Iterator (ForwardSliceSearcher s) Id (Searc
129129
let nextStackPos := stackPos.inc
130130
let nextNeedlePos := needlePos.inc
131131
if h : nextNeedlePos = needle.rawEndPos then
132-
-- Safety: the section from `nextStackPos.descreaseBy needle.utf8ByteSize` to `nextStackPos`
132+
-- Safety: the section from `nextStackPos.decreaseBy needle.utf8ByteSize` to `nextStackPos`
133133
-- (exclusive) is exactly the needle, so it must represent a valid range.
134134
let res := .matched (s.pos! (nextStackPos.decreaseBy needle.utf8ByteSize)) (s.pos! nextStackPos)
135135
-- Invariants still satisfied

tests/lean/run/string_kmp.lean

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -34,3 +34,6 @@ def run (s pat : String) : List S :=
3434
#guard run "𝔸b𝕸xu∅" "𝕸x" = [.r 0 4, .r 4 5, .m 5 10, .r 10 11, .r 11 14]
3535
#guard run "é" "ù" = [.r 0 2]
3636
#guard run "éB" "ù" = [.r 0 2, .r 2 3]
37+
#guard run "abcabdabcabcabcabe" "abcabdabcabe" = [.r 0 6, .r 6 9, .r 9 12, .r 12 15, .r 15 17, .r 17 18]
38+
#guard run "abcabdabcxabcabdabcabe" "abcabdabcabe" = [.r 0 6, .r 6 9, .r 9 10, .m 10 22]
39+
#guard run "€α𝕸€α𝔸€α𝕸€α𝕸€α𝕸€αù" "€α𝕸€α𝔸€α𝕸€αù" = [.r 0 18, .r 18 27, .r 27 36, .r 36 45, .r 45 50, .r 50 52]

0 commit comments

Comments
 (0)