From c1bfc2f042af394da7f9106f79f9bd3fed6d8731 Mon Sep 17 00:00:00 2001 From: Kiana Sheibani Date: Sun, 6 Aug 2023 22:18:11 -0400 Subject: [PATCH] Add partial ratio constructor --- src/Data/Ratio.idr | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/src/Data/Ratio.idr b/src/Data/Ratio.idr index 4caa1c4..d0a0602 100644 --- a/src/Data/Ratio.idr +++ b/src/Data/Ratio.idr @@ -40,9 +40,16 @@ export mkRatioMaybe : IntegralGCD a => (n, d : a) -> Maybe (Ratio a) mkRatioMaybe n d = toMaybe (d /= 0) (reduce $ MkRatio n d) - ||| Create a ratio of two values. -||| WARNING: This is only safe if the denominator is not zero! +export partial +mkRatio : IntegralGCD a => (n, d : a) -> Ratio a +mkRatio n d = case d /= 0 of + True => reduce $ MkRatio n d + +||| Create a ratio of two values, unsafely assuming that they are coprime and +||| the denomindator is non-zero. +||| WARNING: This function will behave erratically and may crash your program +||| if these conditions are not met! export %unsafe unsafeMkRatio : (n, d : a) -> Ratio a unsafeMkRatio = MkRatio