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

Function Not

lean_py/z3/core.py:1337–1338  ·  view source on GitHub ↗
(a: BoolRef)

Source from the content-addressed store, hash-verified

1335
1336
1337def Not(a: BoolRef) -> BoolRef:
1338 return BoolRef(UnOpNode(UnOp.NOT, a._ast), a._vars)
1339
1340
1341def Implies(a: BoolRef, b: BoolRef) -> BoolRef:

Callers 15

checkMethod · 0.90
_applyMethod · 0.90
test_and_or_notMethod · 0.90
test_demorgan_proofMethod · 0.90
test_demorgan2_proofMethod · 0.90
test_contrapositive_proofMethod · 0.90
test_excluded_middleMethod · 0.90
test_xor_definitionMethod · 0.90
test_prove_tautologyMethod · 0.90
test_dependency_chainMethod · 0.90
test_conflictMethod · 0.90
test_is_logical_opsMethod · 0.90

Calls 2

UnOpNodeClass · 0.90
BoolRefClass · 0.85

Tested by 15

test_and_or_notMethod · 0.72
test_demorgan_proofMethod · 0.72
test_demorgan2_proofMethod · 0.72
test_contrapositive_proofMethod · 0.72
test_excluded_middleMethod · 0.72
test_xor_definitionMethod · 0.72
test_prove_tautologyMethod · 0.72
test_dependency_chainMethod · 0.72
test_conflictMethod · 0.72
test_is_logical_opsMethod · 0.72
test_double_negationMethod · 0.72
test_not_reprMethod · 0.72