From 80e43be8fc348abb5450ce77715be2e6a0144a3f Mon Sep 17 00:00:00 2001 From: Kiana Sheibani Date: Fri, 7 Jun 2024 02:07:25 -0400 Subject: [PATCH] Add casting implementations --- src/Data/Ratio.idr | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/src/Data/Ratio.idr b/src/Data/Ratio.idr index 3da1861..a2ed86e 100644 --- a/src/Data/Ratio.idr +++ b/src/Data/Ratio.idr @@ -135,3 +135,18 @@ IntegralGCD a => Fractional (Ratio a) where recip (MkRatio n d) = case n /= 0 of True => MkRatio d n MkRatio n d / MkRatio m b = case m /= 0 of True => reduce $ MkRatio (n*b) (m*d) + +-- ## Casting + +export +Num a => Cast a (Ratio a) where + cast x = MkRatio x 1 + +export +Cast a b => Cast (Ratio a) (Ratio b) where + cast (MkRatio n d) = MkRatio (cast n) (cast d) + +-- Special case: `Cast Rational Double` +export +(Cast a b, Fractional b) => Cast (Ratio a) b where + cast (MkRatio n d) = cast n / cast d