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

Function SubSeq

lean_py/z3/core.py:3950–3952  ·  view source on GitHub ↗

Extract subsequence (alias for SubString).

(s: StringRef, lo: ArithRef | int, length: ArithRef | int)

Source from the content-addressed store, hash-verified

3948
3949
3950def SubSeq(s: StringRef, lo: ArithRef | int, length: ArithRef | int) -> StringRef:
3951 """Extract subsequence (alias for SubString)."""
3952 return SubString(s, lo, length)
3953
3954
3955def SeqMap(f: FuncDeclRef, s: ExprRef) -> ExprRef:

Callers

nothing calls this directly

Calls 1

SubStringFunction · 0.85

Tested by

no test coverage detected