chore: make a global instance local in ModelTheory.Order (#17271)

leanprover-community · Oct 2, 2024 · d902abe · d902abe
1 parent f880a60
commit d902abe
Showing 1 changed file with 8 additions and 4 deletions.
diff --git a/Mathlib/ModelTheory/Order.lean b/Mathlib/ModelTheory/Order.lean
@@ -358,10 +358,14 @@ instance : @OrderedStructure L M _ (L.leOfStructure M) _ := by
   intros
   rfl
 
-instance [h : DecidableRel (fun (a b : M) => Structure.RelMap (leSymb : L.Relations 2) ![a,b])] :
-    DecidableRel (@LE.le M (L.leOfStructure M)) := by
-  letI := L.leOfStructure M
-  exact h
+/-- The order structure on an ordered language is decidable. -/
+-- This should not be a global instance,
+-- because it will match with any `LE` typeclass search
+@[local instance]
+def decidableLEOfStructure
+    [h : DecidableRel (fun (a b : M) => Structure.RelMap (leSymb : L.Relations 2) ![a,b])] :
+    letI := L.leOfStructure M
+    DecidableRel ((· : M) ≤ ·) := h
 
 /-- Any model of a theory of preorders is a preorder. -/
 def preorderOfModels [h : M ⊨ L.preorderTheory] : Preorder M where