Skip to content

Commit

Permalink
fix: delta derived instances now have declaration ranges (leanprover#…
Browse files Browse the repository at this point in the history
…5899)

Fixes an issue where go-to definition on such instances does not work.

Reported [on
Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/mystery.20guest/near/479820367)
  • Loading branch information
kmill authored Oct 31, 2024
1 parent 844e7ae commit f8242fa
Showing 1 changed file with 2 additions and 0 deletions.
2 changes: 2 additions & 0 deletions src/Lean/Elab/Deriving/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@ Authors: Leonardo de Moura, Wojciech Nawrocki
-/
prelude
import Lean.Elab.Command
import Lean.Elab.DeclarationRange

namespace Lean.Elab
open Command
Expand Down Expand Up @@ -55,6 +56,7 @@ def processDefDeriving (className : Name) (declName : Name) : TermElabM Bool :=
safety := info.safety
}
addInstance instName AttributeKind.global (eval_prio default)
addDeclarationRangesFromSyntax instName (← getRef)
return true
catch _ =>
return false
Expand Down

0 comments on commit f8242fa

Please sign in to comment.