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

[Jason Dusek]

On Sat, Feb 12, 2011 at 07:55, Nils Anders Danielsson <nad at chalmers.se> wrote:
> 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.

  The number of constructors? As in, the number of Fin.suc and Fin.zero
  constructors?

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