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.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/data/list/defs.lean

@@ -927,21 +927,9 @@ corresponding element of `as`.
 to_rbmap ['a', 'b', 'c'] = rbmap_of [(0, 'a'), (1, 'b'), (2, 'c')]
 ```
 -/
-def to_rbmap : list α → rbmap ℕ α :=
+def to_rbmap {α : Type*} : list α → rbmap ℕ α :=
 foldl_with_index (λ i mapp a, mapp.insert i a) (mk_rbmap ℕ α)
 
-/--
-`to_rb_map as` is the map that associates each index `i` of `as` with the
-corresponding element of `as`.
-
-```
-to_rb_map ['a', 'b', 'c'] = rb_map.of_list [(0, 'a'), (1, 'b'), (2, 'c')]
-```
--/
-meta def to_rb_map {α : Type} : list α → rb_map ℕ α :=
-foldl_with_index (λ i mapp a, mapp.insert i a) mk_rb_map
-
-
 /-- Auxliary definition used to define `to_chunks`.
 
   `to_chunks_aux n xs i` returns `(xs.take i, (xs.drop i).to_chunks (n+1))`,

src/meta/rb_map.lean

@@ -218,3 +218,18 @@ meta def local_set_to_name_set (lcs : expr_set) : name_set :=
 lcs.fold mk_name_set $ λ h ns, ns.insert h.local_uniq_name
 
 end expr_set
+
+namespace list
+
+/--
+`to_rb_map as` is the map that associates each index `i` of `as` with the
+corresponding element of `as`.
+
+```
+to_rb_map ['a', 'b', 'c'] = rb_map.of_list [(0, 'a'), (1, 'b'), (2, 'c')]
+```
+-/
+meta def to_rb_map {α : Type} : list α → native.rb_map ℕ α :=
+foldl_with_index (λ i mapp a, mapp.insert i a) native.mk_rb_map
+
+end list