Function FiniteDomainSort

lean_py/z3/core.py:4011–4012

(name: str, sz: int, ctx: Context | None = None)

def FiniteDomainSort(name: str, sz: int, ctx: Context | None = None) -> _FiniteDomainSortRef:
    return _FiniteDomainSortRef(name, sz)


def FiniteDomainVal(val: int, sort: SortRef, ctx: Context | None = None) -> ExprRef: