def Lean.Environment.findRedundantImports (env : Environment) (imports : Array Name) : NameSet

Return the redundant imports (i.e. those transitively implied by another import) amongst a candidate list of imports.

Equations

• One or more equations did not get rendered due to their size.

def redundantImports (n? : Option Lean.Name := none) : Lean.CoreM Lean.NameSet

Return the redundant imports (i.e. those transitively implied by another import) of a specified module (or the current module if none is specified).

Equations

• redundantImports n? = do let env ← Lean.getEnv have imports : Array Lean.Name := env.importsOf (n?.getD env.header.mainModule) pure (env.findRedundantImports imports)