monotonicity): replace rb_map.insert_cons
#1571

Merged

chore(meta/rb_map,tactic/monotonicity): replace rb_map.insert_cons #1571

mergify merged 1 commit into master from rem_insert_cons

feat(meta/rb_map,tactic/monotonicity): replace rb_map.insert_cons

72475498

robertylewis changed the title ~~feat(meta/rb_map,tactic/monotonicity): replace rb_map.insert_cons~~ chore(meta/rb_map,tactic/monotonicity): replace rb_map.insert_cons 6 years ago

robertylewis added awaiting-review

cipher1024 approved these changes on 2019-10-20

cipher1024 added ready-to-merge

mergify merged b1654df1 into master 6 years ago

mergify deleted the rem_insert_cons branch 6 years ago

YaelDillies removed awaiting-review

Reviewers

cipher1024

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone

mathlib3 chore(meta/rb_map,tactic/monotonicity): replace rb_map.insert_cons #1571 Merged

chore(meta/rb_map,tactic/monotonicity): replace rb_map.insert_cons #1571

mathlib3
chore(meta/rb_map,tactic/monotonicity): replace rb_map.insert_cons
#1571

Merged