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

Method __init__

lean_py/z3/core.py:903–917  ·  view source on GitHub ↗
(
        self,
        name: str,
        domain: tuple[SortRef, ...],
        range_sort: SortRef,
    )

Source from the content-addressed store, hash-verified

901 __slots__ = ("_name", "_domain", "_range", "_ast_sort")
902
903 def __init__(
904 self,
905 name: str,
906 domain: tuple[SortRef, ...],
907 range_sort: SortRef,
908 ) -> None:
909 self._name = name
910 self._domain = domain
911 self._range = range_sort
912 # Build arrow sort for the function type
913 sorts = [*domain, range_sort]
914 ast_sort: ASTSort = sorts[-1]._ast_sort
915 for s in reversed(sorts[:-1]):
916 ast_sort = ArrowASTSort(s._ast_sort, ast_sort)
917 self._ast_sort = ast_sort
918
919 def __call__(self, *args: ExprRef) -> ExprRef:
920 if len(args) != len(self._domain):

Callers

nothing calls this directly

Calls 1

ArrowASTSortClass · 0.90

Tested by

no test coverage detected