[Agda] FYI: Rationals in Idris

[Sergei Meshveliani]

On Fri, 2015-12-11 at 13:45 +0100, Andreas Abel wrote:
> Nicola Botta told me that he and Tim Richter both implemented rationals 
> in Idris.  See:
> 
>  
> https://github.com/nicolabotta/SeqDecProbs/blob/master/frameworks/14-/NonNegRationalProperties.lidr
> 
>  
> https://github.com/nicolabotta/SeqDecProbs/blob/master/frameworks/14-/NonNegRational2.lidr
> 
> It is not clear yet whether these implementations are efficient enough. 
>   I just post them as a reference in case someone makes a library for 
> rationals in Agda.


Is this for unary coded natural numbers?

Does there exist a library for the arithmetic of natural numbers coded
by a list of macrodigits?

I guess that a few properties of the macrodigit operations need to be
postulated, and the properties of the operations on naturals to be
proved as derived from the algorithm and from the properties of the
macrodigit operations. I expect that this will give that the arithmetic
is fast and that everything is proved, except a few macrodigit
mattters. 
(?)

Thanks,

------
Sergei