Show inferred value for `_` with vscode-lean4

Stream: new members

[Aaron Hill]

If I have an expression like exact h1 _, hovering over the _ in vscode-lean4 will show the inferred type (e.g. N). Is there a way to also show the actual term that was inferred (something like p + 1)? So far, I've been able to figure it out by looking at how the goal changes in the infoview as I move my cursor around, but it would be nice to have a more explicit way of seeing that

[Luigi Massacci]

You can always use show_term, but that is rather brutish

[Luigi Massacci]

Hopefully there is a better way I don't know

[Aaron Hill]

Thanks - that worked. Separately, it looks like hovering has the expected behavior (showing term: type) in most cases, but not for the particular placeholder I was looking at. I'll see if I can come up with a minimized example

[Filippo A. E. Nuccio]

image.png

[Filippo A. E. Nuccio]

I see the name of the term, which version of the lean4 extension are you using?

[Filippo A. E. Nuccio]

Same behaviour online

[Aaron Hill]

I've managed to minimize the issue to this snippet:

theorem bad_lsp (h: ∀ m : Nat, Nat.zero = m) : Nat.zero = (Nat.zero + Nat.zero) := by show_term exact h _

The show_term output is Try this: exact h (Nat.zero + Nat.zero). However, hovering over the _ just shows Nat.
If you replace (Nat.zero + Nat.zero) with (Nat.zero) in the theorem header, then hovering over the _ shows Nat.zero: Nat as expected

[Aaron Hill]

I'll see if I can simplify this any further, then open a bug

[Aaron Hill]

https://github.com/leanprover/lean4/issues/5367

[Filippo A. E. Nuccio]

Wow, and crazily enough if you invert the order as in

theorem bad_lsp (h: ∀ m : Nat, m = Nat.zero) : Nat.zero = (Nat.zero + Nat.zero) := by show_term exact h _

you see the term.