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

Method test_bv_not_not

tests/test_z3_ported.py:691–695  ·  view source on GitHub ↗

~~x == x.

(self, kernel)

Source from the content-addressed store, hash-verified

689 assert prove(claim)
690
691 def test_bv_not_not(self, kernel):
692 """~~x == x."""
693 x = BitVec("x", 8)
694 claim = ForAll([x], ~~x == x)
695 assert prove(claim)
696
697 def test_bv_add_zero(self, kernel):
698 """x + 0 == x."""

Callers

nothing calls this directly

Calls 3

BitVecFunction · 0.90
ForAllFunction · 0.90
proveFunction · 0.90

Tested by

no test coverage detected