This is a library providing a type-safe implementation of permutations. To my knowledge, It is the only such library outside of Coq.
$ idris --install permutations.ipkg
The most useful thing this library provides is a
Group instance for
permutations. You can multiply two elements with
<+>, invert with
an so on.
Show instance for
Permutation uses cycle notation. You can read more
here if you find it confusing.
You can find documentation here.