
  0 | ||| Stuff related to the normal distribution
  1 | module Statistics.Norm
  2 | 
  3 | import public Statistics.Probability
  4 | 
  5 | %default total
  6 | 
  7 | ||| Cumulative distribution function (CDF) of the normal distribution
  8 | public export
  9 | interface NormCDF where
 10 |   normcdf : SolidDouble -> Probability
 11 | 
 12 | ||| Inverse cumulative distribution function of the normal distribution
 13 | public export
 14 | interface InvNormCDF where
 15 |   invnormcdf : Probability -> SolidDouble
 16 |