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

Function SeqSort

lean_py/z3/core.py:3916–3920  ·  view source on GitHub ↗

General sequence sort. For Char, returns StringSort.

(s: SortRef)

Source from the content-addressed store, hash-verified

3914
3915
3916def SeqSort(s: SortRef) -> SeqSortRef | StringSortRef:
3917 """General sequence sort. For Char, returns StringSort."""
3918 if isinstance(s, CharSortRef):
3919 return StringSort()
3920 return SeqSortRef(s)
3921
3922
3923def Empty(s: SortRef) -> ExprRef:

Callers 5

test_seq_sort_charMethod · 0.90
test_empty_seqMethod · 0.90
test_seq_constMethod · 0.90

Calls 2

StringSortFunction · 0.85
SeqSortRefClass · 0.85

Tested by 5

test_seq_sort_charMethod · 0.72
test_empty_seqMethod · 0.72
test_seq_constMethod · 0.72