Skip to main content

discover_lake_modules

lean_toolchain

Function discover_lake_modules 

Source 
pub fn discover_lake_modules(
    options: LeanModuleDiscoveryOptions,
) -> Result<LeanLakeProjectModules, LeanModuleDiscoveryDiagnostic>
Expand description

Discover Lean modules in a Lake project.

ยงErrors

Returns typed diagnostics when the Lake root cannot be found, the active toolchain is unsupported, a selected module root is missing, a module name cannot be represented safely, or source traversal fails.