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

Function CharToInt

lean_py/z3/core.py:3842–3843  ·  view source on GitHub ↗
(ch: ExprRef, ctx: Context | None = None)

Source from the content-addressed store, hash-verified

3840
3841
3842def CharToInt(ch: ExprRef, ctx: Context | None = None) -> ArithRef:
3843 return ArithRef(CharToNatNode(ch._ast), IntSort(), ch._vars)
3844
3845
3846def CharIsDigit(ch: ExprRef, ctx: Context | None = None) -> BoolRef:

Callers 4

test_char_to_intMethod · 0.90
test_char_to_intMethod · 0.90
test_char_to_int_semanticMethod · 0.90
to_intMethod · 0.85

Calls 3

CharToNatNodeClass · 0.90
ArithRefClass · 0.85
IntSortFunction · 0.85

Tested by 3

test_char_to_intMethod · 0.72
test_char_to_intMethod · 0.72
test_char_to_int_semanticMethod · 0.72