(self, *args: ExprRef)
| 917 | self._ast_sort = ast_sort |
| 918 | |
| 919 | def __call__(self, *args: ExprRef) -> ExprRef: |
| 920 | if len(args) != len(self._domain): |
| 921 | raise TypeError(f"{self._name} expects {len(self._domain)} args, got {len(args)}") |
| 922 | merged: frozenset[tuple[str, ASTSort]] = frozenset().union(*(a._vars for a in args)) |
| 923 | # The function itself is a free variable |
| 924 | merged = merged | frozenset([(self._name, self._ast_sort)]) |
| 925 | # Uninterpreted sorts used by the function are also free |
| 926 | # (unless already declared as axioms in the Lean environment) |
| 927 | for s in (*self._domain, self._range): |
| 928 | if isinstance(s, UninterpretedSortRef) and isinstance(s._ast_sort, UninterpASTSort): |
| 929 | if s._ast_sort.name not in _declared_uninterp_sorts: |
| 930 | merged = merged | frozenset([(s._ast_sort.name, TypeASTSort())]) |
| 931 | func_ast = _AstVar(self._name) |
| 932 | args_ast = tuple(a._ast for a in args) |
| 933 | ast = AppNode(func_ast, args_ast) if args else func_ast |
| 934 | return _wrap_expr(ast, self._range, merged) |
| 935 | |
| 936 | def name(self) -> str: |
| 937 | """Return the function name.""" |
nothing calls this directly
no test coverage detected