[Agda] Data.Rational

[Amr Sabry]

Thank you all for your responses. My take is that there are probably
many many ways of implementing rationals and some might be significantly
better than others. There is however not even a baseline implementation
in the current library for simple operations on the rationals. Using the
always-normalized approach that was started in the library, I
implemented the basic operations on rationals (unary negation,
reciprocal, addition, multiplication, and hence trivially subtraction
and division). It's not much but it's start. I am attaching the code in
case someone spots obvious improvements and/or problems. If everything
looks reasonable, I'd be happy to push to the library. Thanks. --Amr

-------------- next part --------------
A non-text attachment was scrubbed...
Name: Rat.agda
Type: application/octet-stream
Size: 7841 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20140323/3004eefe/Rat.obj