Function FiniteDomainVal

lean_py/z3/core.py:4015–4018

(val: int, sort: SortRef, ctx: Context | None = None)

def FiniteDomainVal(val: int, sort: SortRef, ctx: Context | None = None) -> ExprRef:
    if not isinstance(sort, _FiniteDomainSortRef):
        raise TypeError("Expected FiniteDomainSort")
    return ExprRef(FinDomainLit(val, sort._size), sort, frozenset())


def FiniteDomainSize(sort: SortRef, ctx: Context | None = None) -> int: