Definitions on Arrays

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

@[deprecated "This is now in `Mathlib.Tactic.Translate.Reorder.permute!`" (since := "2026-03-05")]

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✝

@[deprecated "This is now in `Mathlib.Tactic.Translate.Reorder.permute!`" (since := "2026-03-05")]

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