max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: temporarily use 100000 as priority

Browse source
This commit is contained in:
Leonardo de Moura 2020-12-15 20:21:27 -08:00
parent 52c815e750
commit 42a28261fd
2 changed files with 10 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Data/Int/Basic.lean
View file

@ -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

18
src/Init/Prelude.lean
View file

@ -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