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

Function StrFromCode

lean_py/z3/core.py:4248–4253  ·  view source on GitHub ↗

Convert character code to single-char string.

(c: ArithRef)

Source from the content-addressed store, hash-verified

4246
4247
4248def StrFromCode(c: ArithRef) -> StringRef:
4249 """Convert character code to single-char string."""
4250 return StringRef(
4251 AppNode(_AstVar("str.from_code"), (c._ast,)),
4252 c._vars,
4253 )
4254
4255
4256def At(s: StringRef, i: ArithRef | int) -> StringRef:

Callers 1

test_str_from_codeMethod · 0.90

Calls 2

AppNodeClass · 0.90
StringRefClass · 0.85

Tested by 1

test_str_from_codeMethod · 0.72