From 358fb280aefaf757402bfe7ce662efb7baf888ce Mon Sep 17 00:00:00 2001
From: rnhmjoj <micheleguerinirocco@me.com>
Date: Wed, 16 Nov 2016 22:06:19 +0100
Subject: [PATCH] add proof for transpose

---
 src/Data/Vec.hs | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/Data/Vec.hs b/src/Data/Vec.hs
index 561cf1b..5d274e6 100644
--- a/src/Data/Vec.hs
+++ b/src/Data/Vec.hs
@@ -175,7 +175,8 @@ intercalate xs xss = concat (intersperse xs xss)
 --
 transpose ∷ SingI n ⇒ Vec (Vec a n) m → Vec (Vec a m) n
 transpose Nil = replicate Nil
-transpose (xs :- xss) = zipWith (:-) xs (transpose xss)
+transpose (xs :- xss) = gcastWith proof (zipWith (:-) xs (transpose xss))
+  where proof = min_self (sLength xs)
 
 
 -- | 'foldl' applied to a binary operator, a starting value