[Agda] how to count 0..n-1

[Nils Anders Danielsson]

On 2011-02-11 06:29, Jason Dusek wrote:
>    Going from a Vec (Fin m) m to a Vec (Fin m+1) m+1 by way of
>    map does seem unattractive, from an operational point of view
>    -- it's n^2 in instead of linear.

I tend not to worry too much about inefficiency when working with unary
numbers. Note, however, that allFin n has a size which is quadratic in
the size of n, so unless we make use of sharing we cannot hope for
better than quadratic complexity.

-- 
/NAD