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_1} [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

• Array.cyclicPermute! x x = match x, x with | a, [] => a | a, i :: is => Array.cyclicPermute!.cyclicPermuteAux a is a[i]! i

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

Equations

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

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

Permute the array using a list of cycles.

Equations

• Array.permute! a ls = List.foldl (fun x x_1 => Array.cyclicPermute! x x_1) a ls