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

[Alan Jeffrey]

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.
>