[Agda] Process: how to extend the Agda standard library?

[Daniel Peebles]

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?

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.

Thanks,
Dan

On Mon, Jun 13, 2011 at 1:46 PM, Alan Jeffrey <ajeffrey at bell-labs.com>wrote:

> If you decide to host your proofs independently, outside the stdlib, then
> there's an agda community on github. https://github.com/agda
>
> A.
>
>
> On 06/13/2011 03:02 AM, Nils Anders Danielsson wrote:
>
>> On 2011-06-10 19:04, Christoph Herrmann wrote:
>>
>>> Anyway, I would like to make the proofs for the properties I am
>>> defining available for everyone in the Agda library. How does the
>>> process work? I assume such changes need to be approved by one of the
>>> main Agda developers to avoid messing up the library.
>>>
>>
>> The process is documented in the README:
>>
>>    http://www.cse.chalmers.se/~nad/listings/lib-0.5/README.html
>>
>> I know of two existing developments proving that the integers form a
>> commutative ring. To avoid duplicated work you may want to start from
>> either of these code bases, and adapt the code so that it fits in with
>> the rest of the library.
>>
>>  _______________________________________________
> 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/20110613/c6c21d92/attachment.html