Data.Permutation

Definitions

record Permutation : Nat -> Type

  A permutation in `n` elements.
  
  Permutations are internally stored as a list of elements to swap in
  right-to-left order. This allows for easy composition and inversion of
  permutation values.

Totality: total
Visibility: export
Constructor: 

MkPerm : List (Fin n, Fin n) -> Permutation n

Projection: 

.swaps : Permutation n -> List (Fin n, Fin n)

Hints:

Mult (Permutation n) (Permutation n) (Permutation n)

MultGroup (Permutation n)

MultMonoid (Permutation n)

Show (Permutation n)

swap : Fin n -> Fin n -> Permutation n

  Construct a permutation that swaps two elements.

Totality: total
Visibility: export

swaps : List (Fin n, Fin n) -> Permutation n

  Construct a permutation that makes the listed swaps in right-to-left order.

Totality: total
Visibility: export

appendSwap : Fin n -> Fin n -> Permutation n -> Permutation n

  Add a swap to the end of a permutation.
  
  `appendSwap sw p = swap sw *. p`

Totality: total
Visibility: export

prependSwap : Fin n -> Fin n -> Permutation n -> Permutation n

  Add a swap to the beginning of a permutation.
  
  `prependSwap sw p = p *. swap sw`

Totality: total
Visibility: export

swapElems : Fin n -> Fin n -> Vect n a -> Vect n a

  Swap two elements of a `Vect`.

Totality: total
Visibility: export

permuteVect : Permutation n -> Vect n a -> Vect n a

  Permute the elements of a `Vect`.

Totality: total
Visibility: export

swapValues : Fin n -> Fin n -> Nat -> Nat

  Construct a function that swaps two values.

Totality: total
Visibility: export

permuteValues : Permutation n -> Nat -> Nat

  Construct a function that permutes values.

Totality: total
Visibility: export