structure Aesop.StatsExtensionEntry : Type

• aesopStx : Lean.Syntax

  The Aesop call for which stats were collected.

• stats : Aesop.Stats

  The collected stats.

@[inline, reducible]

abbrev Aesop.StatsArray : Type

Equations

• Aesop.StatsArray = Array Aesop.StatsExtensionEntry

structure Aesop.StatsExtensionState : Type

• currentEntries : List Aesop.StatsExtensionEntry

  Entries for Aesop calls in the current module.

• currentEntriesSize : Nat

  The size of currentEntries.

• importedEntries : Array (Array Aesop.StatsExtensionEntry)

  Entries for Aesop calls in imported modules.

instance Aesop.instInhabitedStatsExtensionState : Inhabited Aesop.StatsExtensionState

Equations

• Aesop.instInhabitedStatsExtensionState = { default := { currentEntries := default, currentEntriesSize := default, importedEntries := default } }

def Aesop.StatsExtensionState.toStatsArray (s : Aesop.StatsExtensionState) : Aesop.StatsArray

Equations

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

def Aesop.StatsExtensionState.empty : Aesop.StatsExtensionState

Equations

• Aesop.StatsExtensionState.empty = { currentEntries := ∅, currentEntriesSize := 0, importedEntries := ∅ }

instance Aesop.StatsExtensionState.instEmptyCollectionStatsExtensionState : EmptyCollection Aesop.StatsExtensionState

Equations

• Aesop.StatsExtensionState.instEmptyCollectionStatsExtensionState = { emptyCollection := Aesop.StatsExtensionState.empty }

@[inline, reducible]

abbrev Aesop.StatsExtension : Type

Equations

• Aesop.StatsExtension = Lean.PersistentEnvExtension Aesop.StatsExtensionEntry Aesop.StatsExtensionEntry Aesop.StatsExtensionState

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.getStatsArray {m : Type → Type} [Monad m] [Lean.MonadEnv m] : m Aesop.StatsArray

Equations

• Aesop.getStatsArray = do let __do_lift ← Lean.getEnv pure (Aesop.StatsExtensionState.toStatsArray (Lean.PersistentEnvExtension.getState Aesop.statsExtension __do_lift))