def Aesop.sortedPercentileD {α : Type u_1} (p : 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 have 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 → Std.Format)

@[implicit_reducible]

def Aesop.StatsReport.instToStringNanos : ToString Nanos

Equations

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

def Aesop.StatsReport.default : StatsReport

Equations

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

def Aesop.StatsReport.scriptsCore (nSlowest : Nat := 30) (nontrivialOnly : Bool := false) : StatsReport

Equations

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

def Aesop.StatsReport.scripts : StatsReport

Equations

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

def Aesop.StatsReport.scriptsNontrivial : StatsReport

Equations

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