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

Function Cond

lean_py/z3/tactic.py:355–357  ·  view source on GitHub ↗

Conditional tactic: apply t1 if probe p is true, else t2.

(p: Probe, t1: Tactic, t2: Tactic)

Source from the content-addressed store, hash-verified

353
354
355def Cond(p: Probe, t1: Tactic, t2: Tactic) -> Tactic:
356 """Conditional tactic: apply t1 if probe p is true, else t2."""
357 return t1
358
359
360def tactics() -> list[str]:

Callers

nothing calls this directly

Calls

no outgoing calls

Tested by

no test coverage detected