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

Method __init__

lean_py/z3/solver.py:1104–1107  ·  view source on GitHub ↗
(self, opt: Any, is_max: bool, idx: int)

Source from the content-addressed store, hash-verified

1102 """Represents an optimization objective handle."""
1103
1104 def __init__(self, opt: Any, is_max: bool, idx: int) -> None:
1105 self._opt = opt
1106 self._is_max = is_max
1107 self._idx = idx
1108
1109 def lower(self) -> Any:
1110 raise NotImplementedError("OptimizeObjective.lower not supported: Lean is a proof checker")

Callers

nothing calls this directly

Calls

no outgoing calls

Tested by

no test coverage detected