diff --git a/LICENSE b/LICENSE
index 4d48a87..712386e 100644
--- a/LICENSE
+++ b/LICENSE
@@ -1,6 +1,6 @@
 MIT License
 
-Copyright (c) 2022 Kiana Sheibani
+Copyright (c) 2024 Kiana Sheibani
 
 Permission is hereby granted, free of charge, to any person obtaining a copy
 of this software and associated documentation files (the "Software"), to deal
diff --git a/ratio.ipkg b/ratio.ipkg
index 1f426b3..8258a02 100644
--- a/ratio.ipkg
+++ b/ratio.ipkg
@@ -1,4 +1,5 @@
 package ratio
+brief = "Arbitrary-precision ratio types"
 version = 1.0.0
 
 authors = "Kiana Sheibani"
@@ -7,4 +8,5 @@ license = "MIT"
 sourcedir = "src"
 readme = "README.md"
 
-modules = Data.Ratio
+modules = Data.Ratio,
+          Data.IntegralGCD
diff --git a/src/Data/IntegralGCD.idr b/src/Data/IntegralGCD.idr
index 0e2d65d..cd1449b 100644
--- a/src/Data/IntegralGCD.idr
+++ b/src/Data/IntegralGCD.idr
@@ -18,7 +18,7 @@ interface (Eq a, Integral a) => IntegralGCD a where
   gcd x y =
     if x == 0 then y
     else if y == 0 then x
-    else assert_total $ gcd y (x `mod` y)
+    else gcd y (assert_smaller y $ x `mod` y)
 
 
 export IntegralGCD Integer where
diff --git a/src/Data/Ratio.idr b/src/Data/Ratio.idr
index 5487f5c..56dba9f 100644
--- a/src/Data/Ratio.idr
+++ b/src/Data/Ratio.idr
@@ -1,5 +1,6 @@
 module Data.Ratio
 
+import Data.Bool.Xor
 import Data.Maybe
 import Data.So
 import Data.IntegralGCD
@@ -25,35 +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)
-
-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
@@ -78,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
@@ -87,12 +99,12 @@ Eq a => Eq (Ratio a) where
 export
 (Ord a, Num a) => Ord (Ratio a) where
   compare (MkRatio n d) (MkRatio m b) =
-    flipIfNeg (b*d) $ compare (n*b) (m*d)
+    flipIf (b >= 0 `xor` d >= 0) $ compare (n*b) (m*d)
     where
-      flipIfNeg : a -> Ordering -> Ordering
-      flipIfNeg x EQ = EQ
-      flipIfNeg x LT = if x >= 0 then LT else GT
-      flipIfNeg x GT = if x >= 0 then GT else LT
+      flipIf : Bool -> Ordering -> Ordering
+      flipIf _ EQ = EQ
+      flipIf b LT = if b then GT else LT
+      flipIf b GT = if b then LT else GT
 
 export
 Show a => Show (Ratio a) where
@@ -120,3 +132,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