From 0dbd3e6bc89decf9c50cef9fc5d1d66a75f1818c Mon Sep 17 00:00:00 2001
From: Kiana Sheibani <kiana.a.sheibani@gmail.com>
Date: Thu, 6 Jun 2024 20:51:11 -0400
Subject: [PATCH] Use assert_smaller instead of assert_total

---
 src/Data/IntegralGCD.idr | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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