def Lean.Environment.minimalRequiredModules (env : Environment) : Array Name

Return the names of the modules in which constants used in the current file were defined, with modules already transitively imported removed.

Note that this will not account for tactics and syntax used in the file, so the results may not suffice as imports.

Equations

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

def «command#min_imports» : Lean.ParserDescr

Try to compute a minimal set of imports for this file, by analyzing the declarations.

This must be run at the end of the file, and is not aware of syntax and tactics, so the results will likely need to be adjusted by hand.

Equations

• «command#min_imports» = Lean.ParserDescr.node `«command#min_imports» 1024 (Lean.ParserDescr.symbol "#min_imports")

def «command#minimize_imports» : Lean.ParserDescr

Equations

• «command#minimize_imports» = Lean.ParserDescr.node `«command#minimize_imports» 1024 (Lean.ParserDescr.symbol "#minimize_imports")