From 7358df2f7e714a5ad424131290f812dcd80a7cf6 Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Sun, 13 Nov 2022 14:35:37 -0500
Subject: [PATCH] chore: remove `Int.natMod`

---
 src/Init/Data/Int/Basic.lean | 2 --
 1 file changed, 2 deletions(-)

diff --git a/src/Init/Data/Int/Basic.lean b/src/Init/Data/Int/Basic.lean
index c5e16e8122..eabaf743ea 100644
--- a/src/Init/Data/Int/Basic.lean
+++ b/src/Init/Data/Int/Basic.lean
@@ -158,8 +158,6 @@ def toNat : Int → Nat
   | ofNat n   => n
   | negSucc _ => 0
 
-def natMod (m n : Int) : Nat := (m % n).toNat
-
 protected def pow (m : Int) : Nat → Int
   | 0      => 1
   | succ n => Int.pow m n * m