[Agda] Agda2 beginner's question

[Andreas Abel]

Nicolas Pouillard a écrit :
>
>> Maybe I am missing something at 1 a.m. in the night, but the parts of my 
>> brain that are still working tell me that the group function of the 
>> stdlib needs to be rewritten, or at least there needs to be a comment 
>> how on earth you are supposed to use it!
> 
> The original group function *is* usable, 

Sure.  I demonstrated that in my next message.  However, due to wrong 
time stamps my answers are in the wrong order.

> however having a convenient function
> to remove the concat' constructor would help:
> 
> unconcat' : ∀ {a n k} {xs : Vec  a (n * k)} → Group n k xs → Vec (Vec a k) n
> unconcat' (concat' xss) = xss
> 
> group' : ∀ {a} n k (xs : Vec a (n * k)) → Vec (Vec a k) n
> group' n k xs = unconcat' (group n k xs)
> 
> Of course the function names could be improved.
> 


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
http://www.tcs.informatik.uni-muenchen.de/~abel/