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

Equations

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

@[reducible, inline]

abbrev Aesop.StatsExtension : Type

Equations

• Aesop.StatsExtension = Lean.SimplePersistentEnvExtension Aesop.StatsExtensionEntry Unit

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

Equations

• Aesop.StatsExtension.importedEntries env ext = (ext.toEnvExtension.getState env).importedEntries

opaque Aesop.statsExtension : StatsExtension

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

Equations

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

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

Equations

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

@[reducible, inline]

abbrev Aesop.StatsArray : Type

Equations

• Aesop.StatsArray = Array Aesop.StatsExtensionEntry

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

Equations

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

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

Equations

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