Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
import Data.Vect
import Data.Fin
%default total
fins : Vect n (Fin n)
fins {n = Z} = []
fins {n = S n} = FZ :: map FS fins
permutations : {n : Nat} -> Vect (fact n) (Vect n a -> Vect n a)
permutations {n = Z} = [id]
permutations {a = a} {n = S n} =
rewrite multCommutative (S n) (fact n) in
concat $ map inserts (permutations {n = n})
where
inserts : (Vect k a -> Vect k a) -> Vect (S k) (Vect (S k) a -> Vect (S k) a)
inserts pi = map (\i => \(x :: xs) => insertAt i x (pi xs)) fins
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.