From 8c96d213f3089ac2352ed95e79645f4cdbd70ebf Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 14 Aug 2024 15:04:32 +1000 Subject: [PATCH] chore: use local instance in Lsp.Diagnostics (#5031) I'm experimenting with changing the signature of `Ord.arrayOrd`; rather than make a local synonym here, let's make a local instance so it doesn't interact with the experiments. --- src/Lean/Data/Lsp/Diagnostics.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/Lean/Data/Lsp/Diagnostics.lean b/src/Lean/Data/Lsp/Diagnostics.lean index 8740551fa2..da81c222a3 100644 --- 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