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

[Jason Dusek]

On Fri, Feb 11, 2011 at 12:16, Nils Anders Danielsson <nad at chalmers.se> wrote:
> I tend not to worry too much about inefficiency when working
> with unary numbers.

  I grant that this question is more interesting in principle
  than in practice. In systems programming, we might care about
  these things.

> 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. Is this size a
  "type level" thing? It is fine by me to have quadratic
  compiles as long as I have linear runs.

--
Jason Dusek
Linux User #510144 | http://counter.li.org/