@[reducible, inline]

abbrev Aesop.StatsReport : Type

Equations

• Aesop.StatsReport = (Aesop.StatsArray → Lean.Format)

def Aesop.StatsReport.instToStringNanos : ToString Aesop.Nanos

Equations

• Aesop.StatsReport.instToStringNanos = { toString := Aesop.Nanos.printAsMillis }

def Aesop.StatsReport.default : Aesop.StatsReport

Equations

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

def Aesop.StatsReport.default.fmtTime (n : Aesop.Nanos) (samples : Nat) : Lean.Format

Equations

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

def Aesop.StatsReport.default.fmtRuleStats (stats : Array (Aesop.DisplayRuleName × Aesop.RuleStatsTotals)) : Lean.Format

Equations

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