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

Class SeqSortRef

lean_py/z3/core.py:3855–3870  ·  view source on GitHub ↗

Sequence sort.

Source from the content-addressed store, hash-verified

3853
3854
3855class SeqSortRef(SortRef):
3856 """Sequence sort."""
3857
3858 __slots__ = ("_elem",)
3859
3860 def __init__(self, elem: SortRef) -> None:
3861 super().__init__(SeqASTSort(elem._ast_sort))
3862 self._elem = elem
3863
3864 def basis(self) -> SortRef:
3865 """Return the element sort."""
3866 return self._elem
3867
3868 def is_string(self) -> bool:
3869 """True if this is Seq(Char), i.e. String."""
3870 return isinstance(self._elem, CharSortRef)
3871
3872
3873class SeqRef(ExprRef):

Callers 3

_sort_from_ast_sortFunction · 0.85
SeqSortFunction · 0.85
UnitFunction · 0.85

Calls

no outgoing calls

Tested by

no test coverage detected