structure Aesop.StatsExtensionEntry : Type

• aesopStx : Lean.Syntax

  The Aesop call for which stats were collected.

• fileName : String
• position? : Option Lean.Position
• stats : Stats

  The collected stats.

def Aesop.StatsExtensionEntry.forCurrentFile {m : Type → Type} [Monad m] [Lean.MonadLog m] (stx : Lean.Syntax) (stats : Stats) : m StatsExtensionEntry

@[reducible, inline]

abbrev Aesop.StatsExtension : Type

def Aesop.StatsExtension.importedEntries (env : Lean.Environment) (ext : StatsExtension) : Array (Array StatsExtensionEntry)

opaque Aesop.statsExtension : StatsExtension

def Aesop.recordStatsIfEnabled {m : Type → Type} [Monad m] [Lean.MonadEnv m] [Lean.MonadOptions m] (s : StatsExtensionEntry) : m Unit

def Aesop.recordStatsForCurrentFileIfEnabled {m : Type → Type} [Monad m] [Lean.MonadEnv m] [Lean.MonadOptions m] [Lean.MonadLog m] (aesopStx : Lean.Syntax) (stats : Stats) : m Unit

@[reducible, inline]

abbrev Aesop.StatsArray : Type

def Aesop.mkStatsArray (localEntries : List StatsExtensionEntry) (importedEntries : Array (Array StatsExtensionEntry)) : StatsArray

def Aesop.getStatsArray {m : Type → Type} [Monad m] [Lean.MonadEnv m] : m StatsArray