Return definition of a declaration?

Stream: lean4

[Felix Weilacher]

Is there a way to do the following? Given a Name for a declaration, I want to return (as a string, say) the definition of that declaration as written in the code. For, example, on input (`isOpen_iff_of_cover), I want the string pasted here:

lemma isOpen_iff_of_cover {f : α → Set X} (ho : ∀ i, IsOpen (f i)) (hU : (⋃ i, f i) = univ) :
    IsOpen s ↔ ∀ i, IsOpen (f i ∩ s) := by
  refine ⟨fun h i ↦ (ho i).inter h, fun h ↦ ?_⟩
  rw [← s.inter_univ, inter_comm, ← hU, iUnion_inter]
  exact isOpen_iUnion fun i ↦ h i

[Henrik Böving]

That's not generally possible, the original tactic script is not recorded within the .olean files so you'd need to actually have the source file at hand and using declaration location information (which you can get) to obtain the correct substring.

[Felix Weilacher]

About the declaration location information: I know you can get the file name with Evironment.getModuleFor?. Can you get the line numbers?

[Damiano Testa]

You can do this:

import Mathlib

open Lean

/--
info: 'isOpen_iff_of_cover'
start: ⟨113, 0⟩
end:   ⟨117, 33⟩
-/
#guard_msgs in
run_cmd
  let nm := `isOpen_iff_of_cover
  let rg := ((← findDeclarationRanges? nm).getD default).range
  logInfo m!"'{nm}'\nstart: {rg.pos}\nend:   {rg.endPos}"

[Felix Weilacher]

thank you!