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 percentile? stats = match percentile? with | none => stats | some percentile => 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) : Aesop.StatsReport

Equations

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

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 })