- circulate : Permutation n
For S_4, (1234)
Totality: total- cycles : Permutation (S n) -> List (List (Fin (S n)))
Return a list of disjoint cycles given a permutation. We use this for our
pretty-printer.
Totality: total- enumerateStrict : Vect (factorial n) (Permutation n)
All permutations of a certain order.
Totality: total- factorial : Nat -> Nat
- Totality: total
- isEven : Permutation n -> Bool
Test whether a permutation is even.
Totality: total- order : Permutation (S n) -> Nat
- Totality: total
- piPerm : Fin n -> Fin n -> Permutation n
The permutation π_ij
Totality: total- swaps : Permutation n -> List (Permutation n)
Factors a permutation into a product of swaps.
Totality: total