From 7d3ae6c95173e74ecafea68c1a2d8f531ce4852c Mon Sep 17 00:00:00 2001 From: Willem Vanhulle Date: Wed, 15 Apr 2026 19:04:10 +0200 Subject: [PATCH] feat: expose getExtraModUsesInEnv for downstream tooling --- src/Lean/ExtraModUses.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/Lean/ExtraModUses.lean b/src/Lean/ExtraModUses.lean index 34069cafc504..7de5c91944cc 100644 --- a/src/Lean/ExtraModUses.lean +++ b/src/Lean/ExtraModUses.lean @@ -76,6 +76,10 @@ builtin_initialize extraModUses : SimplePersistentEnvExtension ExtraModUse (PHas public def getExtraModUses (env : Environment) (modIdx : ModuleIdx) : Array ExtraModUse := extraModUses.getModuleEntries env modIdx +/-- Returns additional recorded import dependencies of the module currently being elaborated. -/ +public def getExtraModUsesInEnv (env : Environment) : Array ExtraModUse := + (extraModUses.getState (asyncMode := .local) env).fold (init := #[]) fun acc e => acc.push e + /-- Copies additional recorded import dependencies from one environment to another. -/ public def copyExtraModUses (src dest : Environment) : Environment := Id.run do let mut env := dest