`Array.insert` 関数の実装

[Seasawher]

variable {α : Type} 

/--
By swapping elements of the array one by one,
move `xs[old_idx]` to the position `xs[new_idx]`
while preserving the relative order of all other elements.
-/
def Array.insert (xs : Array α) (old_idx new_idx : Nat) (hold: old_idx < xs.size := by decide) (hnew : new_idx < xs.size := by decide) : Array α := Id.run do
  let mut vec := xs.toVector
  if old_idx > new_idx then
    for hi : i in 0...(old_idx - new_idx) do
      vec := vec.swap (old_idx - i) (old_idx - i - 1)
  if old_idx < new_idx then
    for hi : i in 0...(new_idx - old_idx) do
      vec := vec.swap (old_idx + i) (old_idx + i + 1)
  return vec.toArray

#guard #[3, 1, 4, 15, 9, 2].insert 5 2 = #[3, 1, 2, 4, 15, 9]
#guard #[3, 1, 4, 15, 9, 2].insert 1 4 = #[3, 4, 15, 9, 1, 2]