MCPcopy Create free account
hub / github.com/BasisResearch/lean.py / Contains

Function Contains

lean_py/z3/core.py:2294–2298  ·  view source on GitHub ↗

Check if s contains t.

(s: StringRef | SeqRef, t: StringRef | SeqRef)

Source from the content-addressed store, hash-verified

2292
2293
2294def Contains(s: StringRef | SeqRef, t: StringRef | SeqRef) -> BoolRef:
2295 """Check if s contains t."""
2296 if isinstance(s, SeqRef) or isinstance(t, SeqRef):
2297 return BoolRef(SeqContainsNode(s._ast, t._ast), _merge(s._vars, t._vars))
2298 return BoolRef(StrContainsNode(s._ast, t._ast), _merge(s._vars, t._vars))
2299
2300
2301def PrefixOf(pre: StringRef | SeqRef, s: StringRef | SeqRef) -> BoolRef:

Callers 9

test_containsMethod · 0.90
test_containsMethod · 0.90
test_string_free_varsMethod · 0.90
test_contains_groundMethod · 0.90
test_seq_containsMethod · 0.90
test_containsMethod · 0.90
test_contains_emptyMethod · 0.90
test_contains_selfMethod · 0.90

Calls 4

SeqContainsNodeClass · 0.90
StrContainsNodeClass · 0.90
BoolRefClass · 0.85
_mergeFunction · 0.85

Tested by 9

test_containsMethod · 0.72
test_containsMethod · 0.72
test_string_free_varsMethod · 0.72
test_contains_groundMethod · 0.72
test_seq_containsMethod · 0.72
test_containsMethod · 0.72
test_contains_emptyMethod · 0.72
test_contains_selfMethod · 0.72