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

Function FullSet

lean_py/z3/core.py:3617–3619  ·  view source on GitHub ↗

Full set — constant array of True.

(s: SortRef)

Source from the content-addressed store, hash-verified

3615
3616
3617def FullSet(s: SortRef) -> ArrayRef:
3618 """Full set — constant array of True."""
3619 return K(s, BoolVal(True))
3620
3621
3622def IsMember(e: ExprRef, s: ArrayRef) -> BoolRef:

Callers 7

test_full_setMethod · 0.90
test_set_delMethod · 0.90
test_set_intersectMethod · 0.90
test_set_differenceMethod · 0.90
test_is_subsetMethod · 0.90
test_full_setMethod · 0.90
FullFunction · 0.85

Calls 2

KFunction · 0.85
BoolValFunction · 0.85

Tested by 6

test_full_setMethod · 0.72
test_set_delMethod · 0.72
test_set_intersectMethod · 0.72
test_set_differenceMethod · 0.72
test_is_subsetMethod · 0.72
test_full_setMethod · 0.72