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

Function PartialOrder

lean_py/z3/core.py:4364–4367  ·  view source on GitHub ↗

Declare a partial order relation.

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

Source from the content-addressed store, hash-verified

4362
4363
4364def PartialOrder(name: str, ctx: Context | None = None) -> FuncDeclRef:
4365 """Declare a partial order relation."""
4366 s = DeclareSort(name)
4367 return FuncDeclRef(f"{name}_le", (s, s), BoolSort())
4368
4369
4370def LinearOrder(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