Extract tactic sequence from symbol

Stream: lean4

[Leni Aniva]

Given a symbol in the environment, say funext, is there a way to retrieve the sequence of tactics that was used to prove it?

theorem funext {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x}
    (h : ∀ x, f x = g x) : f = g := by
  let eqv (f g : (x : α) → β x) := ∀ x, f x = g x
  let extfunApp (f : Quot eqv) (x : α) : β x :=
    Quot.liftOn f
      (fun (f : ∀ (x : α), β x) => f x)
      (fun _ _ h => h x)
  show extfunApp (Quot.mk eqv f) = extfunApp (Quot.mk eqv g)
  exact congrArg extfunApp (Quot.sound h)

The expression which fulfills the type of funext can be extracted from Environment.constMap, but there is no way to obtain the list of tactics.

I suspect that I would need to tap into the kernel and direct it to parse the source file to find out about the sequence of tactics. Is there a relevant function that does this?

[Scott Morrison]

The full syntax is stored in InfoTree, which you need to go hold of from somewhere. There are examples of processing declarations and doing various things with the Syntax in https://github.com/semorrison/lean-training-data. In particular, if you don't mind recompiling the file that contains the declaration you're interested in, the Frontend.lean in that repository will give you everything you could ask for (Syntax for each declaration, etc).

[Patrick Massot]

Another program doing that is LeanInk.