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

Class _FiniteDomainSortRef

lean_py/z3/core.py:3998–4008  ·  view source on GitHub ↗

Finite domain sort with stored size.

Source from the content-addressed store, hash-verified

3996
3997
3998class _FiniteDomainSortRef(SortRef):
3999 """Finite domain sort with stored size."""
4000
4001 __slots__ = ("_size",)
4002
4003 def __init__(self, name: str, sz: int) -> None:
4004 super().__init__(FinDomainASTSort(sz))
4005 self._size = sz
4006
4007 def size(self) -> int:
4008 return self._size
4009
4010
4011def FiniteDomainSort(name: str, sz: int, ctx: Context | None = None) -> _FiniteDomainSortRef:

Callers 1

FiniteDomainSortFunction · 0.85

Calls

no outgoing calls

Tested by

no test coverage detected