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

Function RecFunction

lean_py/z3/core.py:4035–4037  ·  view source on GitHub ↗

Declare a recursive function.

(name: str, *sorts: SortRef)

Source from the content-addressed store, hash-verified

4033
4034
4035def RecFunction(name: str, *sorts: SortRef) -> FuncDeclRef:
4036 """Declare a recursive function."""
4037 return Function(name, *sorts)
4038
4039
4040def RecAddDefinition(f: FuncDeclRef, args: list[ExprRef], body: ExprRef) -> None:

Callers 2

test_rec_functionMethod · 0.90

Calls 1

FunctionFunction · 0.85

Tested by 2

test_rec_functionMethod · 0.72