English
For vectors of length n, there is a canonical representation by printing as ![a1, a2, ..., an] when α has a Repr.
Русский
Для векторов длины n существует каноническое представление в виде ![a1, a2, ..., an], если у α есть представление Repr.
LaTeX
$$$\\text{There exists a canonical representation of }(\\mathrm{Fin}\\ n \\to \\alpha)\\text{ as }!\\![a_1,\\dots,a_n],$$$
Lean4
/-- Use `![...]` notation for displaying a vector `Fin n → α`, for example:
```
#eval ![1, 2] + ![3, 4] -- ![4, 6]
```
-/
instance _root_.PiFin.hasRepr [Repr α] : Repr (Fin n → α) where
reprPrec f
_ :=
Std.Format.bracket "![" (Std.Format.joinSep ((List.finRange n).map fun n => repr (f n)) ("," ++ Std.Format.line))
"]"
