From 52eb83594b53d23fd388763a74a4cb3ae61540fa Mon Sep 17 00:00:00 2001
From: Kiana Sheibani <kiana.a.sheibani@gmail.com>
Date: Fri, 7 Jun 2024 02:08:31 -0400
Subject: [PATCH] Rearrange sections of Data.Ratio module

---
 src/Data/Ratio.idr | 84 ++++++++++++++++++++++------------------------
 1 file changed, 40 insertions(+), 44 deletions(-)

diff --git a/src/Data/Ratio.idr b/src/Data/Ratio.idr
index 0c63e27..56dba9f 100644
--- a/src/Data/Ratio.idr
+++ b/src/Data/Ratio.idr
@@ -26,50 +26,6 @@ Rational : Type
 Rational = Ratio Integer
 
 
-||| Reduce a ratio by dividing both components by their common factor. Most
-||| operations automatically reduce the returned ratio, so explicitly calling
-||| this function is usually unnecessary.
-export
-reduce : IntegralGCD a => Ratio a -> Ratio a
-reduce (MkRatio n d) =
-  let g = gcd n d in MkRatio (n `div` g) (d `div` g)
-
-
-||| Construct a ratio of two values, returning `Nothing` if the denominator is
-||| zero.
-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.
-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 denominator 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
-
-
-infix 9 //
-
-||| Construct a ratio of two values.
-export
-(//) : IntegralGCD a => (n, d : a) -> {auto 0 ok : So (d /= 0)} -> Ratio a
-(//) n d = reduce $ MkRatio n d
-
-
-||| Round a ratio down to a positive integer.
-export
-floor : Integral a => Ratio a -> a
-floor (MkRatio n d) = n `div` d
-
-
 namespace Ratio
   ||| Return the numerator of the ratio in reduced form.
   export %inline
@@ -94,6 +50,46 @@ namespace Ratio
   (.denom) = dn
 
 
+||| Reduce a ratio by dividing both components by their common factor. Most
+||| operations automatically reduce the returned ratio, so explicitly calling
+||| this function is usually unnecessary.
+export
+reduce : IntegralGCD a => Ratio a -> Ratio a
+reduce (MkRatio n d) =
+  let g = gcd n d in MkRatio (n `div` g) (d `div` g)
+
+||| Construct a ratio of two values, returning `Nothing` if the denominator is
+||| zero.
+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.
+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 denominator 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
+
+infix 9 //
+
+||| Construct a ratio of two values.
+export
+(//) : IntegralGCD a => (n, d : a) -> {auto 0 ok : So (d /= 0)} -> Ratio a
+(//) n d = reduce $ MkRatio n d
+
+
+||| Round a ratio down to the nearest integer less than it.
+export
+floor : Integral a => Ratio a -> a
+floor (MkRatio n d) = n `div` d
 
 
 export