Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-01 00:38 cd457a5d

View on Github →

fix(data/{rbtree,rbmap}): fix some lint errors (#10036)

Estimated changes

Modified src/data/rbmap/default.lean

modified theorem rbmap.eq_leaf_of_max_eq_none

modified theorem rbmap.eq_leaf_of_min_eq_none

Modified src/data/rbtree/basic.lean

modified theorem rbnode.balanced

modified theorem rbnode.depth_min

Modified src/data/rbtree/find.lean

modified theorem rbnode.eqv_of_find_some

Modified src/data/rbtree/insert.lean

modified theorem rbnode.equiv_or_mem_of_mem_ins

modified theorem rbnode.equiv_or_mem_of_mem_insert

modified theorem rbnode.find_balance1_node

modified theorem rbnode.find_balance2_node

modified theorem rbnode.find_black_eq_find_red

modified theorem rbnode.find_ins_of_eqv

modified theorem rbnode.find_insert_of_disj

modified theorem rbnode.find_insert_of_eqv

modified theorem rbnode.find_insert_of_not_eqv

modified theorem rbnode.find_mk_insert_result

modified theorem rbnode.find_red_of_gt

modified theorem rbnode.find_red_of_incomp

modified theorem rbnode.find_red_of_lt

modified theorem rbnode.ins.induction

modified theorem rbnode.ins_ne_leaf

modified theorem rbnode.insert_ne_leaf

modified theorem rbnode.is_searchable_ins

modified theorem rbnode.is_searchable_insert

modified theorem rbnode.ite_eq_of_not_lt

modified theorem rbnode.mem_ins_of_incomp

modified theorem rbnode.mem_ins_of_mem

modified theorem rbnode.mem_insert_of_incomp

modified theorem rbnode.mem_insert_of_mem

modified theorem rbnode.of_mem_balance1_node

modified theorem rbnode.of_mem_balance2_node

Modified src/data/rbtree/main.lean

modified theorem rbtree.balanced

modified theorem rbtree.eq_leaf_of_max_eq_none

modified theorem rbtree.eq_leaf_of_min_eq_none

Modified src/data/rbtree/min_max.lean