Commit 2022-03-08 09:05 a382ac90

View on Github →

feat: Implement Control.Random without streams (#218)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Control/Random.lean

added def IO.runRand

added def Rand.next

added def Rand.range

added def Rand.split

added def Random.rand

added def Random.randBool

added def Random.randBound

added def Random.randFin

Modified Mathlib/Init/Data/Int/Order.lean

added theorem Int.ofNat_natAbs_eq_of_nonneg