From d902abe2c36d37eb76fddd9e43290bcef3bcb6e8 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 2 Oct 2024 05:45:24 +0000 Subject: [PATCH] chore: make a global instance local in ModelTheory.Order (#17271) --- Mathlib/ModelTheory/Order.lean | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/Mathlib/ModelTheory/Order.lean b/Mathlib/ModelTheory/Order.lean index ac41879019da5..af11c905aa569 100644 --- 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