(self, key: str)
| 544 | # invoke `mkEmptyEnvironment` via `parseHeader`) succeed. |
| 545 | # See `lean_py/_runtime.py` for more on why. |
| 546 | if getattr(self.ffi, "lean_io_mark_end_initialization", None) is not None: |
| 547 | self.ffi.lean_io_mark_end_initialization() |
| 548 | |
| 549 | def _load_registry(self) -> LibraryRegistry: |
| 550 | funcs_sym = f"{self.name}_funcs_json" |
| 551 | types_sym = f"{self.name}_types_json" |
| 552 | funcs_json = self._call_string_export(funcs_sym) |
| 553 | types_json = self._call_string_export(types_sym) |
| 554 | return LibraryRegistry.from_json_strings(funcs_json, types_json) |
nothing calls this directly
no outgoing calls
no test coverage detected