From 55d304c7347bba8dcb9e8a5164a056437549e2a8 Mon Sep 17 00:00:00 2001
From: Kiana Sheibani <kiana.a.sheibani@gmail.com>
Date: Wed, 11 May 2022 23:36:31 -0400
Subject: [PATCH] Create Data.Permutation

---
 src/Data/Permutation.idr | 26 ++++++++++++++++++++++++++
 1 file changed, 26 insertions(+)
 create mode 100644 src/Data/Permutation.idr

diff --git a/src/Data/Permutation.idr b/src/Data/Permutation.idr
new file mode 100644
index 0000000..ef8d6ac
--- /dev/null
+++ b/src/Data/Permutation.idr
@@ -0,0 +1,26 @@
+module Data.Permutation
+
+import Data.Vect
+
+%default total
+
+
+public export
+Permutation : Nat -> Type
+Permutation n = Vect n (Fin n)
+
+
+public export
+identity : {n : _} -> Permutation n
+identity {n=Z} = []
+identity {n=S n} = FZ :: map FS identity
+
+public export
+reversed : {n : _} -> Permutation n
+reversed {n=Z} = []
+reversed {n=S n} = last :: map weaken reversed
+
+
+public export
+permuteVect : Permutation n -> Vect n a -> Vect n a
+permuteVect p v = map (\i => index i v) p