feat: save definition sites in code examples

leanprover · Nov 6, 2024 · e706829 · e706829
1 parent dbb71c2
commit e706829
Show file tree

Hide file tree

Showing 3 changed files with 107 additions and 68 deletions.
diff --git a/src/compat/SubVerso/Compat.lean b/src/compat/SubVerso/Compat.lean
@@ -113,6 +113,9 @@ def rwTacticRightBracket? (stx : Syntax) : Option Syntax := Id.run do
   return none
 
 
+def getDeclarationRange? [Monad m] [MonadFileMap m] (stx : Syntax) : m (Option DeclarationRange) :=
+  %first_succeeding [Lean.Elab.getDeclarationRange? stx, some <$> Lean.Elab.getDeclarationRange stx]
+
 namespace List
 -- bind was renamed to flatMap in 4.14
 def flatMap (xs : List α) (f : α → List β) : List β :=