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

Method test_mul_zero

tests/test_z3_semantic.py:874–875  ·  view source on GitHub ↗
(self, kernel)

Source from the content-addressed store, hash-verified

872 assert _try_prove(fpEQ(fpMul(RNE(), FPVal(5.0), FPVal(1.0)), FPVal(5.0)))
873
874 def test_mul_zero(self, kernel):
875 assert _try_prove(fpEQ(fpMul(RNE(), FPVal(5.0), FPVal(0.0)), FPVal(0.0)))
876
877
878class TestFPComparisons:

Callers

nothing calls this directly

Calls 5

_try_proveFunction · 0.90
fpEQFunction · 0.90
fpMulFunction · 0.90
RNEFunction · 0.90
FPValFunction · 0.90

Tested by

no test coverage detected