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

Function _ensure_built

lean_py/_runtime.py:741–748  ·  view source on GitHub ↗

Ensure the runtime types are built (lazy init).

()

Source from the content-addressed store, hash-verified

739 return _LeanFFI # type: ignore[return-value]
740
741
742def get_constants() -> dict[str, int]:
743 """Get the extracted constants."""
744 _ensure_built()
745 return _cached_model.constants # type: ignore[union-attr]
746
747
748@functools.lru_cache(maxsize=1)
749def get_lean_ffi():
750 """Get a singleton LeanFFI instance."""
751 cls = get_ffi_class()

Callers 3

get_structsFunction · 0.85
get_ffi_classFunction · 0.85
get_constantsFunction · 0.85

Calls 3

get_header_modelFunction · 0.90
_build_structsFunction · 0.85
_build_ffi_classFunction · 0.85

Tested by

no test coverage detected