let (xys : Vec m (Vec n X) ---- transpose xys: Vec n (Vec m X)) Why isn't it possible to use Haskell version of transpose as a boilerplate?
transpose [] = [] transpose ([] : xys) = transpose xys transpose ((x:xs):xys) = ... BTW, when I elaborating cases in Epigram, the first case of transpose xys is a vnil (after rec xys then case xys). And, actually, it makes sense to return vnil as an aswer. But Epigram colours return of vnil in brown. >From elaboration information in Epigram buffer I figured out that first vnil case is a transposition to (Vec m (Vec zero X)) and tried recursion on m. It gave me two cases for vnil. First vnil (Vec zero (Vec zero X)) can be transposed into vnil. But second vnil (for result type Vec (suc m) (Vec zero X)) couldn't elaborate preperly. Now I am lost for a little bit longer than in previous questions.
