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

[Nils Anders Danielsson]

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.

-- 
/NAD