<br><div class="gmail_quote">On Wed, Jun 2, 2010 at 10:01 PM, Thorsten Altenkirch <span dir="ltr"><<a href="mailto:txa@cs.nott.ac.uk">txa@cs.nott.ac.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
It seems that it is a feature of Agda that it will run out of memory if you try to formalize category theory :-)<br></blockquote><div><br></div><div>It's for your own protection!</div><div><br></div><div>Seriously though, my suspicion is that the terms you get when formalizing category theory get extremely</div>
<div>large with all the implicit stuff filled in. Being careful to maintain sharing might help with that, but that</div><div>requires some reworking of the internals.</div><div><br></div><div>/ Ulf</div></div>