Permutations.idr

import Data.Vect

%default total

permutations : Vect n a -> Vect (fact n) (Vect n a)
permutations [] = [[]]
permutations {n = S n} (x :: xs) = rewrite multCommutative (S n) (fact n) in
                                   concat $ map (inserts x) (permutations xs)
  where
    inserts : a -> Vect k a -> Vect (S k) (Vect (S k) a)
    inserts x [] = [[x]]
    inserts x (y :: ys) = (x :: y :: ys) :: (map (y ::) (inserts x ys))