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