> 0xN is an empty list > Nx0, the result of the transposition, is a list of N empty lists. You > can express this (the value of N...) with vectors/dependent-types, you > know how long it should be, so you can do this. > > does that seem right?
Yes, but I don't know how to find N it through Epigram. I cannot do case analysis on the length of Vec. I decided to solve that troubling case alone, make transformation from (Vec zero (Vec n X)) to (Vec n (Vec zero X)). I stumbled at the same problem - how to extract length n of (Vec n X) from vnil of (Vec zero (Vec n X)).
