Commit 2020-08-21 00:08 0a48f0a2

View on Github →

feat(system/random): a monad for (pseudo-)randomized computations (#3742)

Estimated changes

added theorem fact.bit0.pos
added theorem fact.bit1.pos
added theorem fact.pow.pos
added theorem fact.succ.pos
modified theorem fin.add_nat_val
added def fin.of_nat'
added theorem fin.val_of_nat_eq_mod'
added theorem fin.val_of_nat_eq_mod
added def bitvec.random
added def bitvec.random_r
added def io.mk_generator
added def io.random
added def io.random_r
added def io.random_series
added def io.run_rand
added def rand.random
added def rand.random_r
added def rand.split
added def rand
added def rand_g.next
added def rand_g
added def shift_31_left