How do I interact with MetaM within a proof?

Stream: metaprogramming / tactics

[nrs]

Suppose my cursor is at the end of the following line in my editor:
example {α} (a : α) (f : α → α) (h : ∀ a, f a = a) : f (f a) = a := by
Is there a way to call Lean.MVarId.getDecl in this context to get info about a metavariable, or is such a call only available when I'm defining a tactic?

[Damiano Testa]

run_tac "opens" the TacticM monad for you: is this close to what you wanted?

[Kyle Miller]

open Lean Meta Elab Tactic

example {α} (a : α) (f : α → α) (h : ∀ a, f a = a) : f (f a) = a := by
  run_tac
    let g ← getMainDecl
    logInfo m!"the type is {g.type}"
    -- the type is f (f a) = a

[nrs]

ah this is exactly it! thank you very much to both!!