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

[Christoph Herrmann]

Hi,

I need to use algebraic laws on integer numbers such as right identity and commutativity in
the attached file. I could not find a comprehensive set of definitions in the Agda standard library 
so I am thinking about how to obtain them.

It seems many of the proofs concerning the semiring properties can make use of the proofs on 
the natural numbers by a comprehensive case distinction, folding/unfolding of the definition,
congruence and refl. Is anyone aware of a generator tool which does such tedious things 
automatically or does anyone have an idea how to do this without a comprehensive case
distinction?

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.

Best Regards


-------------- next part --------------
A non-text attachment was scrubbed...
Name: IntegerProp.agda
Type: application/octet-stream
Size: 1251 bytes
Desc: IntegerProp.agda
Url : http://lists.chalmers.se/pipermail/agda/attachments/20110610/8373d801/IntegerProp.obj
-------------- next part --------------

--
 Dr. Christoph Herrmann
 University of St Andrews, Scotland/UK
 phone: office: +44 1334 461629, home: +44 1334 478648 
 email: cah20 at st-andrews.ac.uk
 URL:   http://www.cs.st-andrews.ac.uk/~ch
 
 The University of St Andrews is a charity registered in Scotland: No SC013532