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

Method test_sub

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

Source from the content-addressed store, hash-verified

839 assert _try_prove(fpEQ(fpAdd(RNE(), FPVal(1.5), FPVal(2.5)), FPVal(4.0)))
840
841 def test_sub(self, kernel):
842 assert _try_prove(fpEQ(fpSub(RNE(), FPVal(5.0), FPVal(3.0)), FPVal(2.0)))
843
844 def test_mul(self, kernel):
845 assert _try_prove(fpEQ(fpMul(RNE(), FPVal(3.0), FPVal(4.0)), FPVal(12.0)))

Callers

nothing calls this directly

Calls 5

_try_proveFunction · 0.90
fpEQFunction · 0.90
fpSubFunction · 0.90
RNEFunction · 0.90
FPValFunction · 0.90

Tested by

no test coverage detected