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

Function ToReal

lean_py/z3/core.py:1659–1665  ·  view source on GitHub ↗

Convert Int to Real.

(x: ArithRef)

Source from the content-addressed store, hash-verified

1657
1658
1659def ToReal(x: ArithRef) -> ArithRef:
1660 """Convert Int to Real."""
1661 return ArithRef(
1662 ToRealNode(x._ast),
1663 RealSort(),
1664 x._vars,
1665 )
1666
1667
1668def ToInt(x: ArithRef) -> ArithRef:

Callers 11

_applyMethod · 0.90
test_mixed_arith_torealMethod · 0.90
test_toreal_astMethod · 0.90
test_torealMethod · 0.90
test_is_to_realMethod · 0.90
test_torealMethod · 0.90
test_int_to_real_groundMethod · 0.90
test_realval_integerMethod · 0.90
test_to_real_preserves_addMethod · 0.90
test_to_real_preserves_mulMethod · 0.90
test_int_to_realMethod · 0.90

Calls 3

ToRealNodeClass · 0.90
ArithRefClass · 0.85
RealSortFunction · 0.85

Tested by 10

test_mixed_arith_torealMethod · 0.72
test_toreal_astMethod · 0.72
test_torealMethod · 0.72
test_is_to_realMethod · 0.72
test_torealMethod · 0.72
test_int_to_real_groundMethod · 0.72
test_realval_integerMethod · 0.72
test_to_real_preserves_addMethod · 0.72
test_to_real_preserves_mulMethod · 0.72
test_int_to_realMethod · 0.72