From 8791efda0cf7392144117cf780bfb6d687d2da5e Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Tue, 4 Jul 2023 12:29:30 +0100
Subject: Add more built-in functions.

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

(limited to 'src/Encoded/Fin.idr')

diff --git a/src/Encoded/Fin.idr b/src/Encoded/Fin.idr
index 0029760..3f369cf 100644
--- a/src/Encoded/Fin.idr
+++ b/src/Encoded/Fin.idr
@@ -40,4 +40,4 @@ forget = Id
 
 export
 divmod' : (k : Nat) -> {auto 0 ok : NonZero k} -> Term (N ~> N * Fin k) ctx
-divmod' k = Abs' (\n => App divmod [<n, Lit k])
+divmod' k = Abs' (\n => App pair [<n `div` Op (Lit k), n `mod` Op (Lit k)])
-- 
cgit v1.2.3