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

Function ToInt

lean_py/z3/core.py:1668–1674  ·  view source on GitHub ↗

Convert Real to Int (floor).

(x: ArithRef)

Source from the content-addressed store, hash-verified

1666
1667
1668def ToInt(x: ArithRef) -> ArithRef:
1669 """Convert Real to Int (floor)."""
1670 return ArithRef(
1671 ToIntNode(x._ast),
1672 IntSort(),
1673 x._vars,
1674 )
1675
1676
1677def Sum(*args: ArithRef) -> ArithRef:

Callers 4

_applyMethod · 0.90
test_tointMethod · 0.90
test_is_to_intMethod · 0.90
test_tointMethod · 0.90

Calls 3

ToIntNodeClass · 0.90
ArithRefClass · 0.85
IntSortFunction · 0.85

Tested by 3

test_tointMethod · 0.72
test_is_to_intMethod · 0.72
test_tointMethod · 0.72