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

Function TreeOrder

lean_py/z3/core.py:4376–4379  ·  view source on GitHub ↗

Declare a tree order relation.

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

Source from the content-addressed store, hash-verified

4374
4375
4376def TreeOrder(name: str, ctx: Context | None = None) -> FuncDeclRef:
4377 """Declare a tree order relation."""
4378 s = DeclareSort(name)
4379 return FuncDeclRef(f"{name}_le", (s, s), BoolSort())
4380
4381
4382def PiecewiseLinearOrder(name: str, ctx: Context | None = None) -> FuncDeclRef:

Callers

nothing calls this directly

Calls 3

DeclareSortFunction · 0.85
FuncDeclRefClass · 0.85
BoolSortFunction · 0.85

Tested by

no test coverage detected