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

Function EmptySet

lean_py/z3/core.py:3612–3614  ·  view source on GitHub ↗

Empty set — constant array of False.

(s: SortRef)

Source from the content-addressed store, hash-verified

3610
3611
3612def EmptySet(s: SortRef) -> ArrayRef:
3613 """Empty set — constant array of False."""
3614 return K(s, BoolVal(False))
3615
3616
3617def FullSet(s: SortRef) -> ArrayRef:

Callers 15

test_empty_setMethod · 0.90
test_is_memberMethod · 0.90
test_set_addMethod · 0.90
test_set_unionMethod · 0.90
test_set_intersectMethod · 0.90
test_set_complementMethod · 0.90
test_set_differenceMethod · 0.90
test_is_subsetMethod · 0.90
test_set_has_size_raisesMethod · 0.90
test_empty_setMethod · 0.90
test_set_addMethod · 0.90
test_is_memberMethod · 0.90

Calls 2

KFunction · 0.85
BoolValFunction · 0.85

Tested by 15

test_empty_setMethod · 0.72
test_is_memberMethod · 0.72
test_set_addMethod · 0.72
test_set_unionMethod · 0.72
test_set_intersectMethod · 0.72
test_set_complementMethod · 0.72
test_set_differenceMethod · 0.72
test_is_subsetMethod · 0.72
test_set_has_size_raisesMethod · 0.72
test_empty_setMethod · 0.72
test_set_addMethod · 0.72
test_is_memberMethod · 0.72