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

Function RatVal

lean_py/z3/core.py:1714–1716  ·  view source on GitHub ↗

Rational value a/b as Real division.

(a: int, b: int)

Source from the content-addressed store, hash-verified

1712
1713
1714def RatVal(a: int, b: int) -> RatNumRef:
1715 """Rational value a/b as Real division."""
1716 return RatNumRef(a, b)
1717
1718
1719Q = RatVal

Callers 15

test_ratval_is_realMethod · 0.90
test_ratval_structureMethod · 0.90
test_ratval_returns_ratnumrefMethod · 0.90
test_numeratorMethod · 0.90
test_denominatorMethod · 0.90
test_numerator_as_longMethod · 0.90
test_denominator_as_longMethod · 0.90
test_as_fractionMethod · 0.90
test_as_stringMethod · 0.90
test_as_longMethod · 0.90
test_ratval_creates_divisionMethod · 0.90
test_ratval_sortMethod · 0.90

Calls 1

RatNumRefClass · 0.85

Tested by 13

test_ratval_is_realMethod · 0.72
test_ratval_structureMethod · 0.72
test_ratval_returns_ratnumrefMethod · 0.72
test_numeratorMethod · 0.72
test_denominatorMethod · 0.72
test_numerator_as_longMethod · 0.72
test_denominator_as_longMethod · 0.72
test_as_fractionMethod · 0.72
test_as_stringMethod · 0.72
test_as_longMethod · 0.72
test_ratval_creates_divisionMethod · 0.72
test_ratval_sortMethod · 0.72