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

[Daniel Peebles]

Whoops! The libraries are https://github.com/copumpkin/categories and
https://github.com/copumpkin/bitvector if anyone's interested in checking
them out.

On Mon, Jun 13, 2011 at 3:30 PM, Daniel Peebles <pumpkingod at gmail.com>wrote:

> 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/3a224582/attachment-0001.html