Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-08-16 13:47 9b2b11f1

View on Github →

refactor(data): stream library was moved back to core lib

Estimated changes

deleted def stream.all
deleted theorem stream.all_def
deleted def stream.any
deleted theorem stream.any_def
deleted theorem stream.append_approx_drop
deleted def stream.apply
deleted def stream.approx
deleted theorem stream.approx_succ
deleted theorem stream.approx_zero
deleted theorem stream.bisim_simple
deleted theorem stream.coinduction
deleted theorem stream.composition
deleted def stream.cons
deleted theorem stream.cons_append_stream
deleted def stream.const
deleted theorem stream.const_eq
deleted def stream.corec'
deleted theorem stream.corec'_eq
deleted def stream.corec
deleted theorem stream.corec_def
deleted theorem stream.corec_eq
deleted def stream.corec_on
deleted def stream.cycle
deleted theorem stream.cycle_eq
deleted theorem stream.cycle_singleton
deleted def stream.drop
deleted theorem stream.drop_append_stream
deleted theorem stream.drop_const
deleted theorem stream.drop_drop
deleted theorem stream.drop_map
deleted theorem stream.drop_succ
deleted theorem stream.drop_zip
deleted theorem stream.eq_of_bisim
deleted def stream.even
deleted theorem stream.even_cons_cons
deleted theorem stream.even_interleave
deleted theorem stream.even_tail
deleted theorem stream.exists_of_mem_map
deleted def stream.head
deleted theorem stream.head_cons
deleted theorem stream.head_even
deleted theorem stream.head_iterate
deleted theorem stream.head_map
deleted theorem stream.head_zip
deleted theorem stream.homomorphism
deleted theorem stream.identity
deleted def stream.inits
deleted def stream.inits_core
deleted theorem stream.inits_core_eq
deleted theorem stream.inits_eq
deleted theorem stream.inits_tail
deleted theorem stream.interchange
deleted def stream.interleave
deleted theorem stream.interleave_eq
deleted def stream.iterate
deleted theorem stream.iterate_eq
deleted theorem stream.iterate_id
deleted def stream.map
deleted theorem stream.map_append_stream
deleted theorem stream.map_cons
deleted theorem stream.map_const
deleted theorem stream.map_eq
deleted theorem stream.map_eq_apply
deleted theorem stream.map_id
deleted theorem stream.map_iterate
deleted theorem stream.map_map
deleted theorem stream.map_tail
deleted theorem stream.mem_cons
deleted theorem stream.mem_cons_of_mem
deleted theorem stream.mem_const
deleted theorem stream.mem_cycle
deleted theorem stream.mem_map
deleted theorem stream.mem_of_mem_even
deleted theorem stream.mem_of_mem_odd
deleted theorem stream.mem_of_nth_eq
deleted def stream.nats
deleted theorem stream.nats_eq
deleted theorem stream.nil_append_stream
deleted def stream.nth
deleted theorem stream.nth_approx
deleted theorem stream.nth_const
deleted theorem stream.nth_drop
deleted theorem stream.nth_even
deleted theorem stream.nth_inits
deleted theorem stream.nth_map
deleted theorem stream.nth_nats
deleted theorem stream.nth_odd
deleted theorem stream.nth_of_bisim
deleted theorem stream.nth_succ
deleted theorem stream.nth_succ_iterate
deleted theorem stream.nth_tails
deleted theorem stream.nth_zero_cons
deleted theorem stream.nth_zero_iterate
deleted theorem stream.nth_zip
deleted def stream.odd
deleted theorem stream.odd_eq
deleted def stream.pure
deleted def stream.tail
deleted theorem stream.tail_cons
deleted theorem stream.tail_const
deleted theorem stream.tail_drop
deleted theorem stream.tail_eq_drop
deleted theorem stream.tail_even
deleted theorem stream.tail_inits
deleted theorem stream.tail_interleave
deleted theorem stream.tail_iterate
deleted theorem stream.tail_map
deleted theorem stream.tail_zip
deleted def stream.tails
deleted theorem stream.tails_eq
deleted theorem stream.tails_eq_iterate
deleted theorem stream.take_theorem
deleted def stream.unfolds
deleted theorem stream.unfolds_eq
deleted theorem stream.unfolds_head_eq
deleted def stream.zip
deleted theorem stream.zip_eq
deleted theorem stream.zip_inits_tails
deleted def stream