Commit 2021-10-23 05:53 183b8c8a

refactor(data/list/defs): move defs about rb_map (#9844) There is nothing intrinsically meta about rb_map, but in practice in mathlib we prove nothing about it and only use it in tactic infrastructure. This PR moves a definition involving rb_map out of data.list.defs and into meta.rb_map (where many others already exist). (motivated by mathport; rb_map is of course disappearing/changing, so better to quarantine this stuff off with other things that aren't being automatically ported) rbmap is not related to rb_map. It can likely be moved from core to mathlib entirely.