def Aesop.StatsArray.filterPercentile {α : Type u_1} [Ord α] (f : Aesop.Stats → α) (percentile : Aesop.Percent) (stats : Aesop.StatsArray) : Aesop.StatsArray

Equations

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

def Aesop.StatsArray.filterOptPercentile {α : Type u_1} [Ord α] (f : Aesop.Stats → α) (percentile? : Option Aesop.Percent) (stats : Aesop.StatsArray) : Aesop.StatsArray

Equations

• Aesop.StatsArray.filterOptPercentile f none stats = stats
• Aesop.StatsArray.filterOptPercentile f (some percentile) stats = Aesop.StatsArray.filterPercentile f percentile stats

@[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.fmtRuleStats (stats : Array (Aesop.DisplayRuleName × Aesop.RuleStatsTotals)) : Lean.Format

Equations

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

def Aesop.StatsReport.scriptsCore (percentile? : optParam (Option Aesop.Percent) none) (nSlowest : optParam Nat 30) : Aesop.StatsReport

def Aesop.StatsReport.scriptsCore.fmtScriptGenerated : Aesop.ScriptGenerated → Lean.Format

Equations

• Aesop.StatsReport.scriptsCore.fmtScriptGenerated Aesop.ScriptGenerated.none = Std.Format.text "<none>"
• Aesop.StatsReport.scriptsCore.fmtScriptGenerated (Aesop.ScriptGenerated.staticallyStructured perfect) = Lean.format "static (perfect: " ++ Lean.format perfect ++ Lean.format ")"
• Aesop.StatsReport.scriptsCore.fmtScriptGenerated (Aesop.ScriptGenerated.dynamicallyStructured perfect) = Lean.format "dynamic (perfect: " ++ Lean.format perfect ++ Lean.format ")"

def Aesop.StatsReport.scripts : Aesop.StatsReport

Equations

• Aesop.StatsReport.scripts = Aesop.StatsReport.scriptsCore

def Aesop.StatsReport.scripts99 : Aesop.StatsReport

Equations

• Aesop.StatsReport.scripts99 = Aesop.StatsReport.scriptsCore (some { toFloat := 0.99 })

def Aesop.StatsReport.scripts95 : Aesop.StatsReport

Equations

• Aesop.StatsReport.scripts95 = Aesop.StatsReport.scriptsCore (some { toFloat := 0.95 })