From 42a28261fde7ea3695657d053d39810b08db41da Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 15 Dec 2020 20:21:27 -0800
Subject: [PATCH] chore: temporarily use `100000` as priority

---
 src/Init/Data/Int/Basic.lean |  2 +-
 src/Init/Prelude.lean        | 18 +++++++++---------
 2 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/src/Init/Data/Int/Basic.lean b/src/Init/Data/Int/Basic.lean
index a7ca2c1003..b97c5ea505 100644
--- a/src/Init/Data/Int/Basic.lean
+++ b/src/Init/Data/Int/Basic.lean
@@ -60,7 +60,7 @@ protected def mul (m n : @& Int) : Int :=
   | negSucc m, ofNat n   => negOfNat (succ m * n)
   | negSucc m, negSucc n => ofNat (succ m * succ n)
 
-@[defaultInstance 10]
+@[defaultInstance 100000]
 instance : Neg Int where
   neg := Int.neg
 instance : Add Int where
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index 0035db2443..1ca33f1c6b 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -417,39 +417,39 @@ class OrElse (α : Type u) where
 class AndThen (α : Type u) where
   andThen : α → α → α
 
-@[defaultInstance 10]
+@[defaultInstance 100000] -- use high
 instance [Add α] : HAdd α α α where
   hAdd a b := Add.add a b
 
-@[defaultInstance 10]
+@[defaultInstance 100000]
 instance [Sub α] : HSub α α α where
   hSub a b := Sub.sub a b
 
-@[defaultInstance 10]
+@[defaultInstance 100000]
 instance [Mul α] : HMul α α α where
   hMul a b := Mul.mul a b
 
-@[defaultInstance 10]
+@[defaultInstance 100000]
 instance [Div α] : HDiv α α α where
   hDiv a b := Div.div a b
 
-@[defaultInstance 10]
+@[defaultInstance 100000]
 instance [Mod α] : HMod α α α where
   hMod a b := Mod.mod a b
 
-@[defaultInstance 10]
+@[defaultInstance 100000]
 instance [Pow α] : HPow α α α where
   hPow a b := Pow.pow a b
 
-@[defaultInstance 10]
+@[defaultInstance 100000]
 instance [Append α] : HAppend α α α where
   hAppend a b := Append.append a b
 
-@[defaultInstance 10]
+@[defaultInstance 100000]
 instance [OrElse α] : HOrElse α α α where
   hOrElse a b := OrElse.orElse a b
 
-@[defaultInstance 10]
+@[defaultInstance 100000]
 instance [AndThen α] : HAndThen α α α where
   hAndThen a b := AndThen.andThen a b