structure Aesop.StatsFileRecordextends Aesop.Stats : Type

• total : Nanos
• configParsing : Nanos
• ruleSetConstruction : Nanos
• search : Nanos
• ruleSelection : Nanos
• script : Nanos
• scriptGenerated : Option ScriptGenerated
• ruleStats : Array RuleStats
• file : String
• position : Option Lean.Position

instance Aesop.instToJsonStatsFileRecord : Lean.ToJson StatsFileRecord

Equations

• Aesop.instToJsonStatsFileRecord = { toJson := Aesop.instToJsonStatsFileRecord.toJson }

def Aesop.instToJsonStatsFileRecord.toJson : StatsFileRecord → Lean.Json

Equations

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

def Aesop.StatsFileRecord.ofStats {m : Type → Type} [Monad m] [Lean.MonadLog m] (aesopStx : Lean.Syntax) (stats : Stats) : m StatsFileRecord

Equations

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

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

Equations

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