Are there any existing implementations of rational numbers in Idris?
E.g. Data.Ratio ports from Haskell.
Data.Ratio
With a quick search, I found this, if it could be interesting