From 29dc5c5b1b43c84a101da8c0c16603c3fcb16779 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20G=2E=20Dorais?= <fgdorais@gmail.com>
Date: Mon, 31 May 2021 06:52:12 -0400
Subject: [PATCH] fix: duplicate namespace prefix

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

diff --git a/src/Init/Data/Int/Basic.lean b/src/Init/Data/Int/Basic.lean
index a40b134884..f09be2bf6e 100644
--- a/src/Init/Data/Int/Basic.lean
+++ b/src/Init/Data/Int/Basic.lean
@@ -160,7 +160,7 @@ def toNat : Int → Nat
 
 def natMod (m n : Int) : Nat := (m % n).toNat
 
-protected def Int.pow (m : Int) : Nat → Int
+protected def pow (m : Int) : Nat → Int
   | 0      => 1
   | succ n => Int.pow m n * m