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

Method test_rounding_mode_long_names

tests/test_z3_ported.py:3854–3859  ·  view source on GitHub ↗
(self)

Source from the content-addressed store, hash-verified

3852 assert isinstance(RTZ(), FPRMRef)
3853
3854 def test_rounding_mode_long_names(self):
3855 assert isinstance(RoundNearestTiesToEven(), FPRMRef)
3856 assert isinstance(RoundNearestTiesToAway(), FPRMRef)
3857 assert isinstance(RoundTowardPositive(), FPRMRef)
3858 assert isinstance(RoundTowardNegative(), FPRMRef)
3859 assert isinstance(RoundTowardZero(), FPRMRef)
3860
3861 def test_fp_add(self):
3862 x, y = FPs("x y", Float32())

Callers

nothing calls this directly

Calls 5

RoundNearestTiesToEvenFunction · 0.90
RoundNearestTiesToAwayFunction · 0.90
RoundTowardPositiveFunction · 0.90
RoundTowardNegativeFunction · 0.90
RoundTowardZeroFunction · 0.90

Tested by

no test coverage detected