Skip to content

Commit

Permalink
Remove HasSubsequence
Browse files Browse the repository at this point in the history
  • Loading branch information
p-offtermatt committed Oct 10, 2023
1 parent f46554b commit 3630846
Showing 1 changed file with 0 additions and 24 deletions.
24 changes: 0 additions & 24 deletions tests/difference/core/quint_model/libraries/extraSpells.qnt
Original file line number Diff line number Diff line change
Expand Up @@ -187,30 +187,6 @@ module extraSpells {
assert(min(Set(1, 2, 3)) == 1),
}

pure def HasSubsequence(__this: List[a], __other: List[a]): bool = {
if(__other.length() > __this.length()) {
false
} else {
0.to(__this.length() - __other.length()) // go through all possible starting points of __other in __this
.exists(
__start => __this.slice(__start, __start + __other.length()) == __other
)
}
}

run HasSubsequenceTest =
all {
assert(List(1, 2, 3, 4).HasSubsequence(List(1, 2))),
assert(List(1, 2, 3, 4).HasSubsequence(List(2, 3))),
assert(List(1, 2, 3, 4).HasSubsequence(List(3, 4))),
assert(List(1, 2, 3, 4).HasSubsequence(List(1, 2, 3))),
assert(not(List(1, 2, 3, 4).HasSubsequence(List(1, 3)))),
assert(not(List().HasSubsequence(List(1)))),
assert(List().HasSubsequence(List())),
assert(List(1).HasSubsequence(List())),
assert(List(1).HasSubsequence(List(1))),
}

// Returns the maximum element of a set, according to a given function.
// If two elements are equally large, an arbitrary one will be returned.
// If the set is empty, the function call will fail at runtime.
Expand Down

0 comments on commit 3630846

Please sign in to comment.