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

Function WithParams

lean_py/z3/tactic.py:345–347  ·  view source on GitHub ↗

Apply tactic with params (returns tactic unchanged).

(t: Tactic, p: object)

Source from the content-addressed store, hash-verified

343
344
345def WithParams(t: Tactic, p: object) -> Tactic:
346 """Apply tactic with params (returns tactic unchanged)."""
347 return t
348
349
350def When(p: Probe, t: Tactic) -> Tactic:

Callers

nothing calls this directly

Calls

no outgoing calls

Tested by

no test coverage detected