Yeah, unary numbers aren't the best representation for efficiency :P<br><br><div class="gmail_quote">On Sat, Feb 12, 2011 at 10:03 AM, Jason Dusek <span dir="ltr"><<a href="mailto:jason.dusek@gmail.com">jason.dusek@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;"><div class="im">On Sat, Feb 12, 2011 at 07:55, Nils Anders Danielsson <<a href="mailto:nad@chalmers.se">nad@chalmers.se</a>> wrote:<br>
> On 2011-02-12 04:14, Jason Dusek wrote:<br>
> ><br>
> > On Fri, Feb 11, 2011 at 12:16, Nils Anders Danielsson<<a href="mailto:nad@chalmers.se">nad@chalmers.se</a>> wrote:<br>
> > > Note, however, that allFin n has a size which is quadratic in<br>
> > > the size of n, so unless we make use of sharing we cannot hope for<br>
> > > better than quadratic complexity.<br>
> ><br>
> > I don't understand -- it's size is quadratic in the size of n?<br>
> > I guess I don't know what you mean by size.<br>
><br>
> The number of constructors.<br>
<br>
</div> The number of constructors? As in, the number of Fin.suc and Fin.zero<br>
constructors?<br>
<div class="im"><br>
--<br>
Jason Dusek<br>
Linux User #510144 | <a href="http://counter.li.org/" target="_blank">http://counter.li.org/</a><br>
_______________________________________________<br>
</div><div><div></div><div class="h5">Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br>