Idris2Doc : Profile.Statistics

Profile.Statistics

(source)
Definitions
mean : Vect (S n) (Scalar u) -> Scalar u
  Totality: total
  Visibility: public export
record Stats : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkStats : AttoSecondsPerRun -> AttoSecondsPerRun -> Double -> Stats

  Projections:
  
.mean : Stats -> AttoSecondsPerRun
  
.r2 : Stats -> Double
  
.slope : Stats -> AttoSecondsPerRun
.slope : Stats -> AttoSecondsPerRun
  Totality: total
  Visibility: public export
slope : Stats -> AttoSecondsPerRun
  Totality: total
  Visibility: public export
.mean : Stats -> AttoSecondsPerRun
  Totality: total
  Visibility: public export
mean : Stats -> AttoSecondsPerRun
  Totality: total
  Visibility: public export
.r2 : Stats -> Double
  Totality: total
  Visibility: public export
r2 : Stats -> Double
  Totality: total
  Visibility: public export
regr : Vect (S n) Measured -> Stats
  Totality: total
  Visibility: export