chore: use local instance in Lsp.Diagnostics

2026-04-04 19:24:09 +00:00 · 2024-08-14 14:49:42 +10:00
1 changed files with 1 additions and 2 deletions
--- a/src/Lean/Data/Lsp/Diagnostics.lean
+++ b/src/Lean/Data/Lsp/Diagnostics.lean
@@ -113,8 +113,7 @@ structure DiagnosticWith (α : Type) where
 def DiagnosticWith.fullRange (d : DiagnosticWith α) : Range :=
  d.fullRange?.getD d.range

-local instance [Ord α] : Ord (Array α) := Ord.arrayOrd
-
+attribute [local instance] Ord.arrayOrd in
 /-- Restriction of `DiagnosticWith` to properties that are displayed to users in the InfoView. -/
 private structure DiagnosticWith.UserVisible (α : Type) where
  range               : Range