← Copula mathematical handbook

def Lean.Compiler.LCNF.collectUsedDecls (decls : Array Name) : CoreM (Array (Decl Purity.impure) × Array (Signature Purity.impure))

Find all declarations that the declarations in decls transitively depend on. They are returned partitioned into the declarations from the current module and declarations from other modules.

Equations

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

def Lean.Compiler.LCNF.usesModuleFrom (env : Environment) (modulePrefix : Name) : Bool

Equations

• Lean.Compiler.LCNF.usesModuleFrom env modulePrefix = env.header.modules.any fun (mod : Lean.EffectiveImport) => mod.irPhases != Lean.IRPhases.comptime && modulePrefix.isPrefixOf mod.module