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

Method calc_enter

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

Source from the content-addressed store, hash-verified

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)
113 return TacticResult.parse(encoded, self._kernel, next_state)
114
115 def fragment_exit(self) -> TacticResult:
116 encoded, next_state = self._kernel._lib.leanpy_kernel_goal_fragment_exit(self._handle)

Callers

nothing calls this directly

Calls 1

parseMethod · 0.80

Tested by

no test coverage detected