Mathlib Changelog
Changelog
About
Github
Commit
2020-08-21 00:08
0a48f0a2
View on Github →
feat(system/random): a monad for (pseudo-)randomized computations (
#3742
)
Estimated changes
Modified
src/control/monad/basic.lean
added
def
reader_t.equiv
added
def
state_t.equiv
added
def
state_t.eval
Modified
src/control/monad/cont.lean
added
def
cont_t.equiv
Modified
src/control/monad/writer.lean
added
def
writer_t.equiv
Created
src/control/uliftable.lean
added
def
cont_t.uliftable'
added
def
reader_t.uliftable'
added
def
state_t.uliftable'
added
def
uliftable.adapt_down
added
def
uliftable.adapt_up
added
def
uliftable.down
added
def
uliftable.down_map
added
theorem
uliftable.down_up
added
def
uliftable.up
added
theorem
uliftable.up_down
added
def
uliftable.up_map
added
def
writer_t.uliftable'
Created
src/data/bitvec/basic.lean
added
theorem
bitvec.add_lsb_div_two
added
theorem
bitvec.add_lsb_eq_twice_add_one
added
def
bitvec.of_fin
added
theorem
bitvec.of_fin_le_of_fin_of_le
added
theorem
bitvec.of_fin_to_fin
added
theorem
bitvec.of_fin_val
added
theorem
bitvec.of_nat_to_nat
added
theorem
bitvec.to_bool_add_lsb_mod_two
added
def
bitvec.to_fin
added
theorem
bitvec.to_fin_le_to_fin_of_le
added
theorem
bitvec.to_fin_of_fin
added
theorem
bitvec.to_fin_val
added
theorem
bitvec.to_nat_eq_foldr_reverse
added
theorem
bitvec.to_nat_lt
Modified
src/data/bool.lean
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
Modified
src/data/fin.lean
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
Modified
src/data/nat/basic.lean
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
nat.pow_succ_log_gt_self
Modified
src/data/stream/basic.lean
added
def
stream.corec_state
added
theorem
stream.length_take
added
def
stream.take
Modified
src/set_theory/lists.lean
Created
src/system/random/basic.lean
added
def
bitvec.random
added
def
bitvec.random_r
added
theorem
bool_of_nat_mem_Icc_of_mem_Icc_to_nat
added
def
io.mk_generator
added
def
io.random
added
def
io.random_r
added
def
io.random_series
added
def
io.random_series_r
added
def
io.run_rand
added
def
rand.random
added
def
rand.random_r
added
def
rand.random_series
added
def
rand.random_series_r
added
def
rand.split
added
def
rand
added
def
rand_g.next
added
def
rand_g
added
def
random_fin_of_pos
added
def
shift_31_left
Created
test/slim_check.lean
added
def
find_prime
added
def
find_prime_aux
added
def
iterated_primality_test
added
def
iterated_primality_test_aux
added
def
primality_test