From 6dddcde25cf76f2e9dee3083370d04bcb8287efa Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 7 Dec 2020 16:58:34 -0800 Subject: [PATCH] chore: increase priority of `defaultInstance` for heterogeneous operators @Kha The motivation is to allow users to define default instances such as ```lean @[defaultInstance 1] instance : OfScientific Real where ... ``` Then, numerals such as `1.2` and `3.4e10` will be `Real` by default instead of `Float`. --- src/Init/Prelude.lean | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index 1df0eef242..1f80379d62 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -414,39 +414,39 @@ class OrElse (α : Type u) where class AndThen (α : Type u) where andThen : α → α → α -@[defaultInstance 1] +@[defaultInstance 10] instance [Add α] : HAdd α α α where hAdd a b := Add.add a b -@[defaultInstance 1] +@[defaultInstance 10] instance [Sub α] : HSub α α α where hSub a b := Sub.sub a b -@[defaultInstance 1] +@[defaultInstance 10] instance [Mul α] : HMul α α α where hMul a b := Mul.mul a b -@[defaultInstance 1] +@[defaultInstance 10] instance [Div α] : HDiv α α α where hDiv a b := Div.div a b -@[defaultInstance 1] +@[defaultInstance 10] instance [Mod α] : HMod α α α where hMod a b := Mod.mod a b -@[defaultInstance 1] +@[defaultInstance 10] instance [Pow α] : HPow α α α where hPow a b := Pow.pow a b -@[defaultInstance 1] +@[defaultInstance 10] instance [Append α] : HAppend α α α where hAppend a b := Append.append a b -@[defaultInstance 1] +@[defaultInstance 10] instance [OrElse α] : HOrElse α α α where hOrElse a b := OrElse.orElse a b -@[defaultInstance 1] +@[defaultInstance 10] instance [AndThen α] : HAndThen α α α where hAndThen a b := AndThen.andThen a b