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

Daniel Peebles pumpkingod at gmail.com
Sat Feb 12 16:01:28 CET 2011


Yeah, unary numbers aren't the best representation for efficiency :P

On Sat, Feb 12, 2011 at 10:03 AM, Jason Dusek <jason.dusek at gmail.com> wrote:

> 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/
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20110212/20d6ceaa/attachment.html


More information about the Agda mailing list