structure Aesop.StatsFileRecordextends Aesop.Stats : Type

• total : Nanos
• configParsing : Nanos
• ruleSetConstruction : Nanos
• search : Nanos
• ruleSelection : Nanos
• script : Nanos
• forwardState : Nanos
• scriptGenerated : Option ScriptGenerated
• ruleStats : Array RuleStats
• goalStats : Array GoalStats
• syntax : String
• file : String
• position : Option Lean.Position
• declaration : Option Lean.Name
• goalSolved : Bool

@[implicit_reducible]

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] [Lean.Elab.MonadParentDecl m] [MonadLiftT Lean.CoreM m] (aesopStx : Lean.Syntax) (goalSolved : Bool) (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] [Lean.Elab.MonadParentDecl m] [MonadLiftT IO m] [MonadLiftT Lean.CoreM m] (aesopStx : Lean.Syntax) (stats : Stats) (allGoalsSolved : Bool) : m Unit

Equations

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