some more instance priority changes

leanprover-community · May 9, 2024 · 99bc417 · 99bc417
1 parent 08e4eb0
commit 99bc417
Show file tree

Hide file tree

Showing 2 changed files with 13 additions and 0 deletions.
diff --git a/Mathlib/Algebra/Order/Kleene.lean b/Mathlib/Algebra/Order/Kleene.lean
@@ -414,3 +414,13 @@ protected abbrev kleeneAlgebra [KleeneAlgebra α] [Zero β] [One β] [Add β] [M
 #align function.injective.kleene_algebra Function.Injective.kleeneAlgebra
 
 end Function.Injective
+
+-- lower instance priorities to avoid instance synthesis trying this early
+attribute [instance 50] IdemSemiring.toSemiring
+attribute [instance 50] IdemCommSemiring.toCommSemiring
+
+-- add higer-priority versions in scope `AlgebraOrderInstances`
+namespace AlgebraOrderInstances
+attribute [scoped instance 200] IdemSemiring.toSemiring
+attribute [scoped instance 200] IdemCommSemiring.toCommSemiring
+end AlgebraOrderInstances
diff --git a/Mathlib/Algebra/Ring/BooleanRing.lean b/Mathlib/Algebra/Ring/BooleanRing.lean
@@ -617,3 +617,6 @@ instance : BooleanRing Bool where
   mul_zero a := by cases a <;> rfl
   nsmul := nsmulRec
   zsmul := zsmulRec
+
+-- lower instance priority to avoid instance synthesis trying this early
+attribute [instance 50] BooleanRing.toRing