feat(data/fin/vec_notation): add has_reflect instance and tests (#14670)

src/data/fin/vec_notation.lean

@@ -74,7 +74,7 @@ variables {m n : ℕ}
 #eval ![1, 2] + ![3, 4] -- ![4, 6]
 ```
 -/
-instance pi_fin.has_repr [has_repr α] : has_repr (fin n → α) :=
+instance _root_.pi_fin.has_repr [has_repr α] : has_repr (fin n → α) :=
 { repr := λ f, "![" ++ (string.intercalate ", " ((list.fin_range n).map (λ n, repr (f n)))) ++ "]" }
 
 end matrix_notation
@@ -146,6 +146,12 @@ by { refine fin.forall_fin_one.2 _ i, refl }
 lemma cons_fin_one (x : α) (u : fin 0 → α) : vec_cons x u = (λ _, x) :=
 funext (cons_val_fin_one x u)
 
+meta instance _root_.pi_fin.reflect {α : Type} [reflected α] [h : has_reflect α] :
+  Π {n}, has_reflect (fin n → α)
+| 0 v := (subsingleton.elim vec_empty v).rec (`(λ a, @vec_empty.{0} a).subst `(α))
+| (n + 1) v := (cons_head_tail v).rec $
+  (`(λ x (xs : fin n → α), vec_cons x xs).subst (h _)).subst (_root_.pi_fin.reflect _)
+
 /-! ### Numeral (`bit0` and `bit1`) indices
 The following definitions and `simp` lemmas are to allow any
 numeral-indexed element of a vector given with matrix notation to

test/vec_notation.lean

@@ -0,0 +1,22 @@
+import data.fin.vec_notation
+
+/-! These tests are testing `pi_fin.reflect` and fail with
+`local attribute [-instance] pi_fin.reflect` -/
+
+#eval do
+  let x : fin 0 → ℕ := ![],
+  tactic.is_def_eq `(x) `(![] : fin 0 → ℕ)
+
+#eval do
+  let x := ![1, 2, 3],
+  tactic.is_def_eq `(x) `(![1, 2, 3])
+
+#eval do
+  let x := ![![1, 2], ![3, 4]],
+  tactic.is_def_eq `(x) `(![![1, 2], ![3, 4]])
+
+/-! These tests are testing `pi_fin.has_repr` -/
+
+#eval show tactic unit, from guard (repr (![] : _ → ℕ) = "![]")
+#eval show tactic unit, from guard (repr ![1, 2, 3] = "![1, 2, 3]")
+#eval show tactic unit, from guard (repr ![![1, 2], ![3, 4]] = "![![1, 2], ![3, 4]]")