Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-30 01:45 fcc158e9

View on Github →

chore(*): update to Lean-3.35.0c (#9988) Move stream, rbtree, and rbmap from core to mathlib and reflows some long lines. Rename some files to avoid name clashes.

Estimated changes

added def mk_rbmap
added def rbmap.contains
added def rbmap.empty
added def rbmap.find
added def rbmap.find_entry
added def rbmap.fold
added def rbmap.from_list
added def rbmap.insert
added def rbmap.max
added def rbmap.min
added def rbmap.rev_fold
added def rbmap.to_list
added def rbmap.to_value
added def rbmap
added def rbmap_lt
added def rbmap_of
added theorem rbmap.find_correct
added theorem rbmap.find_insert
added theorem rbmap.max_is_maximal
added theorem rbmap.mem_insert
added theorem rbmap.mem_of_find_some
added theorem rbmap.mem_of_max_eq
added theorem rbmap.mem_of_min_eq
added theorem rbmap.min_is_minimal
added theorem rbmap.not_mem_mk_rbmap
added theorem rbmap.not_mem_of_empty
added theorem rbnode.balanced
added theorem rbnode.depth_max'
added theorem rbnode.depth_max
added theorem rbnode.depth_min
added inductive rbnode.is_node_of
added inductive rbnode.is_red_black
added inductive rbnode.is_searchable
added def rbnode.lift
added theorem rbnode.lo_lt_hi
added theorem rbnode.lt_of_mem_left
added theorem rbnode.lt_of_mem_right
added theorem rbnode.range
added theorem rbnode.find.induction
added theorem rbnode.find_correct
added def mk_rbtree
added def rbnode.balance1
added def rbnode.balance2
added inductive rbnode.color
added def rbnode.depth
added def rbnode.find
added def rbnode.fold
added def rbnode.get_color
added def rbnode.ins
added def rbnode.insert
added def rbnode.mem
added def rbnode.mem_exact
added def rbnode.rev_fold
added inductive rbnode.well_formed
added inductive rbnode
added def rbtree.contains
added def rbtree.depth
added def rbtree.empty
added def rbtree.find
added def rbtree.fold
added def rbtree.from_list
added def rbtree.insert
added def rbtree.mem_exact
added def rbtree.rev_fold
added def rbtree.to_list
added def rbtree
added def rbtree_of
added theorem rbnode.balance.cases
added theorem rbnode.balance1_eq₁
added theorem rbnode.balance1_eq₂
added theorem rbnode.balance1_eq₃
added theorem rbnode.balance1_rb
added theorem rbnode.balance2_eq₁
added theorem rbnode.balance2_eq₂
added theorem rbnode.balance2_eq₃
added theorem rbnode.balance2_rb
added theorem rbnode.find_ins_of_eqv
added theorem rbnode.find_red_of_gt
added theorem rbnode.find_red_of_lt
added theorem rbnode.ins.induction
added theorem rbnode.ins_ne_leaf
added theorem rbnode.ins_rb
added theorem rbnode.insert_ne_leaf
added theorem rbnode.insert_rb
added inductive rbnode.is_bad_red_black
added theorem rbnode.mem_ins_of_mem
added theorem rbtree.balanced
added theorem rbtree.eq_of_find_some
added theorem rbtree.find_correct
added theorem rbtree.find_insert
added theorem rbtree.max_is_maximal
added theorem rbtree.mem_insert
added theorem rbtree.mem_of_max_eq
added theorem rbtree.mem_of_min_eq
added theorem rbtree.min_is_minimal
added theorem rbnode.max_is_maximal
added theorem rbnode.mem_of_max_eq
added theorem rbnode.mem_of_min_eq
added theorem rbnode.min_is_minimal
added def stream.all
added theorem stream.all_def
added def stream.any
added theorem stream.any_def
added def stream.apply
added def stream.approx
added theorem stream.approx_succ
added theorem stream.approx_zero
added theorem stream.bisim_simple
added theorem stream.coinduction
added theorem stream.composition
added def stream.cons
added def stream.const
added theorem stream.const_eq
added def stream.corec'
added theorem stream.corec'_eq
added def stream.corec
added theorem stream.corec_def
added theorem stream.corec_eq
added def stream.corec_on
added def stream.cycle
added theorem stream.cycle_eq
added theorem stream.cycle_singleton
added def stream.drop
added theorem stream.drop_const
added theorem stream.drop_drop
added theorem stream.drop_map
added theorem stream.drop_succ
added theorem stream.drop_zip
added theorem stream.eq_of_bisim
added def stream.even
added theorem stream.even_cons_cons
added theorem stream.even_interleave
added theorem stream.even_tail
added def stream.head
added theorem stream.head_cons
added theorem stream.head_even
added theorem stream.head_iterate
added theorem stream.head_map
added theorem stream.head_zip
added theorem stream.homomorphism
added theorem stream.identity
added def stream.inits
added theorem stream.inits_core_eq
added theorem stream.inits_eq
added theorem stream.inits_tail
added theorem stream.interchange
added theorem stream.interleave_eq
added def stream.iterate
added theorem stream.iterate_eq
added theorem stream.iterate_id
added def stream.map
added theorem stream.map_cons
added theorem stream.map_const
added theorem stream.map_eq
added theorem stream.map_eq_apply
added theorem stream.map_id
added theorem stream.map_iterate
added theorem stream.map_map
added theorem stream.map_tail
added theorem stream.mem_cons
added theorem stream.mem_cons_of_mem
added theorem stream.mem_const
added theorem stream.mem_cycle
added theorem stream.mem_map
added theorem stream.mem_of_mem_even
added theorem stream.mem_of_mem_odd
added theorem stream.mem_of_nth_eq
added def stream.nats
added theorem stream.nats_eq
added def stream.nth
added theorem stream.nth_approx
added theorem stream.nth_const
added theorem stream.nth_drop
added theorem stream.nth_even
added theorem stream.nth_inits
added theorem stream.nth_map
added theorem stream.nth_nats
added theorem stream.nth_odd
added theorem stream.nth_of_bisim
added theorem stream.nth_succ
added theorem stream.nth_tails
added theorem stream.nth_zero_cons
added theorem stream.nth_zip
added def stream.odd
added theorem stream.odd_eq
added def stream.pure
added def stream.tail
added theorem stream.tail_cons
added theorem stream.tail_const
added theorem stream.tail_drop
added theorem stream.tail_eq_drop
added theorem stream.tail_even
added theorem stream.tail_inits
added theorem stream.tail_interleave
added theorem stream.tail_iterate
added theorem stream.tail_map
added theorem stream.tail_zip
added def stream.tails
added theorem stream.tails_eq
added theorem stream.take_theorem
added def stream.unfolds
added theorem stream.unfolds_eq
added theorem stream.unfolds_head_eq
added def stream.zip
added theorem stream.zip_eq
added theorem stream.zip_inits_tails
added def stream