@@ -436,12 +436,12 @@ intercalate sep xss = concat $ intersperse sep xss
437||| transpose [[], [1, 2]] = [[1], [2]]
437||| transpose [[], [1, 2]] = [[1], [2]]
438||| transpose (transpose [[], [1, 2]]) = [[1, 2]]
438||| transpose (transpose [[], [1, 2]]) = [[1, 2]]
440−||| TODO: Solution which satisfies the totality checker?
441transpose : List (List a) -> List (List a)
439transpose : List (List a) -> List (List a)
442transpose [] = []
440transpose [] = []
443−transpose ([] :: xss) = transpose xss
441+transpose (heads :: tails) = spreadHeads heads (transpose tails) where
444−transpose ((x::xs) :: xss) = assert_total $ (x :: (mapMaybe head' xss)) :: (transpose (xs :: (map (drop 1) xss)))
442+ spreadHeads [] tails = tails
443+ spreadHeads (head :: heads) [] = [head] :: spreadHeads heads []
444+ spreadHeads (head :: heads) (tail :: tails) = (head :: tail) :: spreadHeads heads tails
446--------------------------------------------------------------------------------
446--------------------------------------------------------------------------------
447-- Membership tests
447-- Membership tests