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

Method test_empty_seq

tests/test_z3_compat.py:2060–2065  ·  view source on GitHub ↗

Empty(SeqSort) creates a SeqRef.

(self)

Source from the content-addressed store, hash-verified

2058 assert isinstance(s, StringSortRef)
2059
2060 def test_empty_seq(self):
2061 """Empty(SeqSort) creates a SeqRef."""
2062
2063 s = SeqSort(IntSort())
2064 e = Empty(s)
2065 assert isinstance(e, SeqRef)
2066
2067 def test_unit_seq(self):
2068 """Unit creates a SeqRef from a non-string element."""

Callers

nothing calls this directly

Calls 3

SeqSortFunction · 0.90
IntSortFunction · 0.90
EmptyFunction · 0.90

Tested by

no test coverage detected