Statistics.Probability

Reexports

Definitions

data Probability : Type

Totality: total
Visibility: public export
Constructor: 

P : DoubleBetween 0.0 1.0 -> Probability

Hints:

Cast Probability Double

Cast Probability (DoubleBetween 0.0 1.0)

Cast (DoubleBetween 0.0 1.0) Probability

Eq Probability

Monoid Probability

Ord Probability

Semigroup Probability

Show Probability

fromDouble : (x : Double) -> {auto 0 _ : So ((0.0 <= x) && Delay (x <= 1.0))} -> Probability

Totality: total
Visibility: public export

fromInteger : (n : Integer) -> {auto 0 _ : Either (n = 0) (n = 1)} -> Probability

Totality: total
Visibility: public export

.asDouble : Probability -> Double

Totality: total
Visibility: public export

.value : Probability -> DoubleBetween 0.0 1.0

Totality: total
Visibility: public export

maybeP : Double -> Maybe Probability

Totality: total
Visibility: public export

(/) : (num : Double) -> (den : Double) -> {auto 0 _ : So ((1.0 < num) && Delay (num <= den))} -> Probability

Totality: total
Visibility: export
Fixity Declaration: infixl operator, level 9

ratio : (num : Nat) -> (den : Nat) -> {auto 0 _ : LTE num den} -> {auto 0 _ : IsSucc den} -> Probability

Totality: total
Visibility: export

successesRatio : Fin (S den) -> {auto 0 _ : IsSucc den} -> Probability

Totality: total
Visibility: export

.percent : DoubleBetween 0.0 100 -> Probability

Totality: total
Visibility: public export

(*) : Probability -> Probability -> Probability

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 9

(/) : Probability -> DoubleBetween 1.0 (1.0 / 0.0) -> Probability

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 9

inv : Probability -> Probability

Totality: total
Visibility: public export

.inv : Probability -> Probability

Totality: total
Visibility: public export