From fdbc5b9d69c0dcb17d26c589d81eebfc8543acde Mon Sep 17 00:00:00 2001
From: Kiana Sheibani <kiana.a.sheibani@gmail.com>
Date: Sun, 6 Aug 2023 22:10:47 -0400
Subject: [PATCH] Add unsafe ratio constructor

---
 src/Data/Ratio.idr | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/src/Data/Ratio.idr b/src/Data/Ratio.idr
index 5487f5c..4caa1c4 100644
--- a/src/Data/Ratio.idr
+++ b/src/Data/Ratio.idr
@@ -40,6 +40,14 @@ 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 %unsafe
+unsafeMkRatio : (n, d : a) -> Ratio a
+unsafeMkRatio = MkRatio
+
+
 infix 9 //
 
 ||| Construct a ratio of two values.