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.

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ₙ]

Equations

• x.cyclicPermute! [] = x
• x.cyclicPermute! (i :: is) = Array.cyclicPermute!.cyclicPermuteAux x is x[i]! i

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

Equations

• Array.cyclicPermute!.cyclicPermuteAux x✝¹ [] x✝ x = x✝¹.set! x x✝
• Array.cyclicPermute!.cyclicPermuteAux x✝¹ (i :: is) x✝ x = match x✝¹.swapAt! i x✝ with | (y, a) => Array.cyclicPermute!.cyclicPermuteAux a is y x

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

Permute the array using a list of cycles.

Equations

• a.permute! ls = List.foldl (fun (x1 : Array α) (x2 : List Nat) => x1.cyclicPermute! x2) a ls