Names of constants defined in current file

Stream: lean4

[Adam Topaz]

Do we have an efficient way to obtain the names of constants that have been defined up to a certain point but just in the current file? right now I'm using the following, but it's too slow with larger imports:

import Mathlib.Lean.Expr.Basic
import Lean

open Lean

def constsInFile : CoreM Unit := do
  let env ← getEnv
  let mut newCs : Array (Name × ConstantInfo) := #[]
  for (n,c) in env.constants do
    if ← n.isBlackListed then continue
    if let none := env.getModuleIdxFor? n then newCs := newCs.push (n,c)
  for (n,_) in newCs do
    println! n

[Kyle Miller]

Yes, take a look at how whatsnew works -- there's a map containing just the module's constants.

[Adam Topaz]

Oh great! It's just ConstMap.map\_2.