[Agda] FYI: Rationals in Idris

[Andreas Abel]

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.

Cheers,
Andreas

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/