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

Function At

lean_py/z3/core.py:4256–4260  ·  view source on GitHub ↗

Character at index i as a single-char string.

(s: StringRef, i: ArithRef | int)

Source from the content-addressed store, hash-verified

4254
4255
4256def At(s: StringRef, i: ArithRef | int) -> StringRef:
4257 """Character at index i as a single-char string."""
4258 if isinstance(i, int):
4259 i = IntVal(i)
4260 return SubString(s, i, IntVal(1))
4261
4262
4263def Diff(a: ReRef, b: ReRef) -> ReRef:

Callers 2

test_atMethod · 0.90
test_at_int_literalMethod · 0.90

Calls 2

IntValFunction · 0.85
SubStringFunction · 0.85

Tested by 2

test_atMethod · 0.72
test_at_int_literalMethod · 0.72