add proof for transpose
This commit is contained in:
parent
c631d24d38
commit
358fb280ae
@ -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
|
||||
|
Loading…
Reference in New Issue
Block a user