Definitions on Arrays

This file contains various definitions on Array. It does not contain proofs about these definitions, those are contained in other files in Mathlib/Data/Array.lean.

def Array.cyclicPermute! {α : Type u} [Inhabited α] : Array α → List Nat → 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 Nat → α → Nat → Array α

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

Permute the array using a list of cycles.