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 = match x✝, x with | a, [] => a | a, i :: is => Array.cyclicPermute!.cyclicPermuteAux a is a[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 (x : Array α) (x_1 : List Nat) => x.cyclicPermute! x_1) a ls