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
.
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ₙ]
Instances For
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