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

Method instantiate_all

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

Source from the content-addressed store, hash-verified

401 return self._lib.leanpy_kernel_delab_unfold_matchers(src)
402
403 def instantiate_all(self, src: str) -> str:
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)

Callers 2

mainFunction · 0.95

Calls

no outgoing calls

Tested by 1