Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-21 00:08 0a48f0a2

View on Github →

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

Estimated changes

added def reader_t.equiv
added def state_t.equiv
added def state_t.eval
added def cont_t.equiv
added def writer_t.equiv
added def uliftable.down
added theorem uliftable.down_up
added def uliftable.up
added theorem uliftable.up_down
added def uliftable.up_map
added theorem bitvec.add_lsb_div_two
added def bitvec.of_fin
added theorem bitvec.of_fin_to_fin
added theorem bitvec.of_fin_val
added theorem bitvec.of_nat_to_nat
added def bitvec.to_fin
added theorem bitvec.to_fin_of_fin
added theorem bitvec.to_fin_val
added theorem bitvec.to_nat_lt
added def bool.of_nat
added theorem bool.of_nat_le_of_nat
added theorem bool.of_nat_to_nat
added def bool.to_nat
added theorem bool.to_nat_le_to_nat
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 nat.log
added theorem nat.log_pow
added theorem nat.pow_le_iff_le_log
added theorem nat.pow_log_le_self
added theorem stream.length_take
added def stream.take
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
added def find_prime
added def find_prime_aux
added def primality_test