def Aesop.sortedPercentileD {α : Type u_1} (p : Aesop.Percent) (dflt : α) (xs : Array α) : α

Assumes that xs is ascending. We use a simple nearest-rank definition of percentiles.

Equations

• Aesop.sortedPercentileD p dflt xs = if (xs.size == 0) = true then dflt else let rank := (xs.size.toFloat * p.toFloat).ceil.toUInt64.toNat.min (xs.size - 1); xs[rank]?.getD dflt

def Aesop.sortedMedianD {α : Type u_1} (dflt : α) (xs : Array α) : α

Equations

• Aesop.sortedMedianD dflt xs = Aesop.sortedPercentileD { toFloat := 0.5 } dflt xs

@[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

• Aesop.StatsReport.default.fmtTime n samples = Lean.format "" ++ Lean.format n ++ Lean.format " [" ++ Lean.format (if (samples == 0) = true then 0 else n / samples) ++ Lean.format "]"

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 (nSlowest : optParam Nat 30) (nontrivialOnly : optParam Bool false) : Aesop.StatsReport

Equations

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

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 hasMVar) = Lean.format "static (perfect: " ++ Lean.format perfect ++ Lean.format ")"
• Aesop.StatsReport.scriptsCore.fmtScriptGenerated (Aesop.ScriptGenerated.dynamicallyStructured perfect hasMVar) = Lean.format "dynamic (perfect: " ++ Lean.format perfect ++ Lean.format ")"

def Aesop.StatsReport.scriptsCore.fmtTimes (ns : Array Aesop.Nanos) : Lean.Format

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.scriptsNontrivial : Aesop.StatsReport

Equations

• Aesop.StatsReport.scriptsNontrivial = Aesop.StatsReport.scriptsCore 30 true