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

[Nils Anders Danielsson]

On 2011-02-12 04:14, Jason Dusek wrote:
> On Fri, Feb 11, 2011 at 12:16, Nils Anders Danielsson<nad at chalmers.se>  wrote:
>> 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.
>
>    I don't understand -- it's size is quadratic in the size of n?
>    I guess I don't know what you mean by size.

The number of constructors.

-- 
/NAD