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

Function LastIndexOf

lean_py/z3/core.py:4230–4236  ·  view source on GitHub ↗

Find last index of substr in s.

(s: StringRef, substr: StringRef)

Source from the content-addressed store, hash-verified

4228
4229
4230def LastIndexOf(s: StringRef, substr: StringRef) -> ArithRef:
4231 """Find last index of substr in s."""
4232 return ArithRef(
4233 AppNode(_AstVar("str.last_indexof"), (s._ast, substr._ast)),
4234 IntSort(),
4235 _merge(s._vars, substr._vars),
4236 )
4237
4238
4239def StrToCode(s: StringRef) -> ArithRef:

Callers 1

test_last_index_ofMethod · 0.90

Calls 4

AppNodeClass · 0.90
ArithRefClass · 0.85
IntSortFunction · 0.85
_mergeFunction · 0.85

Tested by 1

test_last_index_ofMethod · 0.72