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

Method test_set_difference

tests/test_z3_compat.py:2022–2028  ·  view source on GitHub ↗

SetDifference creates an array expression.

(self)

Source from the content-addressed store, hash-verified

2020 assert isinstance(s, ExprRef)
2021
2022 def test_set_difference(self):
2023 """SetDifference creates an array expression."""
2024
2025 a = SetAdd(EmptySet(IntSort()), IntVal(1))
2026 b = EmptySet(IntSort())
2027 d = SetDifference(a, b)
2028 assert isinstance(d, ExprRef)
2029
2030 def test_is_subset(self):
2031 """IsSubset creates a BoolRef."""

Callers

nothing calls this directly

Calls 5

SetAddFunction · 0.90
EmptySetFunction · 0.90
IntSortFunction · 0.90
IntValFunction · 0.90
SetDifferenceFunction · 0.90

Tested by

no test coverage detected