Whoops! The libraries are <a href="https://github.com/copumpkin/categories">https://github.com/copumpkin/categories</a> and <a href="https://github.com/copumpkin/bitvector">https://github.com/copumpkin/bitvector</a> if anyone's interested in checking them out.<br>
<br><div class="gmail_quote">On Mon, Jun 13, 2011 at 3:30 PM, Daniel Peebles <span dir="ltr"><<a href="mailto:pumpkingod@gmail.com">pumpkingod@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
Anyone have any objections to me adding a category theory library James Deikun and I have been working on for a while to that github organization?<div><br></div><div>I was also thinking of putting the bitvector (binary naturals mod 2^n and lots of associated proofs and algebraic structures) library that Eric Mertens and I worked on a while back on there, if there are no objections.</div>
<div><br></div><div>Thanks,</div><div>Dan<div><div></div><div class="h5"><br><br><div class="gmail_quote">On Mon, Jun 13, 2011 at 1:46 PM, Alan Jeffrey <span dir="ltr"><<a href="mailto:ajeffrey@bell-labs.com" target="_blank">ajeffrey@bell-labs.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">If you decide to host your proofs independently, outside the stdlib, then there's an agda community on github. <a href="https://github.com/agda" target="_blank">https://github.com/agda</a><br>
<font color="#888888">
<br>
A.</font><div><br>
<br>
On 06/13/2011 03:02 AM, Nils Anders Danielsson wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
On 2011-06-10 19:04, Christoph Herrmann wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Anyway, I would like to make the proofs for the properties I am<br>
defining available for everyone in the Agda library. How does the<br>
process work? I assume such changes need to be approved by one of the<br>
main Agda developers to avoid messing up the library.<br>
</blockquote>
<br>
The process is documented in the README:<br>
<br>
<a href="http://www.cse.chalmers.se/~nad/listings/lib-0.5/README.html" target="_blank">http://www.cse.chalmers.se/~nad/listings/lib-0.5/README.html</a><br>
<br>
I know of two existing developments proving that the integers form a<br>
commutative ring. To avoid duplicated work you may want to start from<br>
either of these code bases, and adapt the code so that it fits in with<br>
the rest of the library.<br>
<br>
</blockquote></div><div><div></div><div>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">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></div></div></div>
</blockquote></div><br>