[Agda] FYI: Rationals in Idris

[Dr. ÉRDI Gergő]

I hope this might be useful to someone as well:
http://stackoverflow.com/questions/31212459/how-to-add-two-rational-in-agda/31265445#31265445
On 11 Dec 2015 20:46, "Andreas Abel" <abela at chalmers.se> 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.
>
> 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/
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20151211/d4b9b103/attachment.html