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

Method try_tactic

lean_py/kernel.py:99–101  ·  view source on GitHub ↗
(self, tactic: str)

Source from the content-addressed store, hash-verified

97 return self._kernel._lib.leanpy_kernel_goal_pretty(self._handle)
98
99 def try_tactic(self, tactic: str) -> TacticResult:
100 encoded, next_state = self._kernel._lib.leanpy_kernel_goal_try_tactic(self._handle, tactic)
101 return TacticResult.parse(encoded, self._kernel, next_state)
102
103 def try_assign(self, expr: str) -> TacticResult:
104 encoded, next_state = self._kernel._lib.leanpy_kernel_goal_try_assign(self._handle, expr)

Callers 4

_verify_exprFunction · 0.95
_try_proveFunction · 0.80
applyMethod · 0.80
mainFunction · 0.80

Calls 1

parseMethod · 0.80

Tested by

no test coverage detected