`Array.reshape` 関数を Vector にする

これを Vector α (m * n) からの関数にしたくなるのが人情であるが、これが意外と大変だったりする。

実際、こういう関数を実装したいときはどうするのが良いのだろうか？現在のベストプラクティスを調べてみたいところ。

/-- 配列を二次元配列に変換する。
サイズが期待と異なる場合は `panic!` を呼ぶ -/
def Array.reshape (m n : Nat) (xs : Array α) : Array (Array α) :=
  if xs.size ≠ m * n then
    panic! s!"{decl_name%}: size mismatch"
  else
    Array.range m |>.map (fun i => xs.extract (n * i) (n * (i + 1)))

#guard
  let actual := Array.reshape (m := 2) (n := 3) #[1, 2, 3, 4, 5, 6]
  let expected := #[#[1, 2, 3], #[4, 5, 6]]
  actual == expected

The issue names no repository file or test; start with the Array.reshape example and compare the requested Vector signature with the existing Array behavior. Determine the current best practice for handling the size mismatch and confirm that the provided guard example still expresses the expected result.