See synthesized argument

Stream: lean4

[Nir Paz]

Is there a way to see what argument lean inserted in an _? Hovering over it only shows the type. For example in

example (n : ℕ) : n ^ 2 = n ^ 2 := Eq.refl _

I want to see n ^ 2 is the argument used for Eq.refl.

[Mario Carneiro]

lean4#5367

[Patrick Massot]

You can use by show_term Eq.refl _.

[Thomas Murrills]

By the way, this seems like a special case of this discussion: #lean4 > Pre-RFC: Forcing terms to be shown in hover? (I never did make an RFC, though, so I’ll simply comment on the GitHub issue linked above.)