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

Method expr_proj_to_app

lean_py/kernel.py:406–407  ·  view source on GitHub ↗
(self, src: str)

Source from the content-addressed store, hash-verified

404 return self._lib.leanpy_kernel_delab_instantiate_all(src)
405
406 def expr_proj_to_app(self, src: str) -> str:
407 return self._lib.leanpy_kernel_delab_expr_proj_to_app(src)
408
409
410__all__ = ["Kernel", "GoalState", "TacticResult"]

Calls

no outgoing calls