Definitions on Arrays

This file contains various definitions on Array. It does not contain proofs about these definitions.

def Array.cyclicPermute! {α : Type u} [Inhabited α] : Array α → List ℕ → Array α

Permute the array using a sequence of indices defining a cyclic permutation. If the list of indices l = [i₁, i₂, ..., iₙ] are all distinct then (cyclicPermute! a l)[iₖ₊₁] = a[iₖ] and (cyclicPermute! a l)[i₀] = a[iₙ]

def Array.cyclicPermute!.cyclicPermuteAux {α : Type u} : Array α → List ℕ → α → ℕ → Array α

def Array.permute! {α : Type u} [Inhabited α] (a : Array α) (ls : List (List ℕ)) : Array α

Permute the array using a list of cycles.