structure Aesop.StatsExtensionEntry : Type

• aesopStx : Lean.Syntax

  The Aesop call for which stats were collected.

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

  The collected stats.

def Aesop.StatsExtensionEntry.forCurrentFile {m : Type → Type} [Monad m] [Lean.MonadLog m] (stx : Lean.Syntax) (stats : Aesop.Stats) : m Aesop.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 : Aesop.StatsExtension) : Array (Array Aesop.StatsExtensionEntry)

Equations

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

opaque Aesop.statsExtension : Aesop.StatsExtension

def Aesop.recordStatsIfEnabled {m : Type → Type} [Monad m] [Lean.MonadEnv m] [Lean.MonadOptions m] (s : Aesop.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 : Aesop.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 Aesop.StatsExtensionEntry) (importedEntries : Array (Array Aesop.StatsExtensionEntry)) : Aesop.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 Aesop.StatsArray

Equations

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