[Agda] Agda student's research

[Sergei Meshveliani]

On Mon, 2014-12-29 at 13:06 +0100, Peter Divianszky wrote:
> Hello,
> 
> Recently I began an informal Agda course at my workplace.
> One of the participants is a mathematics student at ELTE Budapest 
> University.
> So far he likes Agda a lot and he plans to start an Agda
> development which would do symbolic derivation with correctness proofs.
> He could start with polynomials over a ring.
> 
> My question is, do you know of similar developments in Agda?
> 


Before implementing a provable derivation for polynomials over a ring, 
needs one to have done provable arithmetic for polynomials over a ring?
For example, for a commutative ring R, one probably needs to implement a
provable commutative ring instance for polynomials over R. 
Need such things to be done before derivation?

------
Sergei