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

Method conv_enter

lean_py/kernel.py:107–109  ·  view source on GitHub ↗
(self)

Source from the content-addressed store, hash-verified

105 return TacticResult.parse(encoded, self._kernel, next_state)
106
107 def conv_enter(self) -> TacticResult:
108 encoded, next_state = self._kernel._lib.leanpy_kernel_goal_conv_enter(self._handle)
109 return TacticResult.parse(encoded, self._kernel, next_state)
110
111 def calc_enter(self) -> TacticResult:
112 encoded, next_state = self._kernel._lib.leanpy_kernel_goal_calc_enter(self._handle)

Callers

nothing calls this directly

Calls 1

parseMethod · 0.80

Tested by

no test coverage detected