Hover and `fun` type information

Stream: lean4

[Damiano Testa]

Dear All,

after seeing the thread about the parentheses, I thought that today might be a good day to ask another similar question.

In this code

import Mathlib.Tactic.RunCmd

open Lean in
run_cmd do  -- prints `fun IamANat ↦ Bool`, hovering on `IamANat` shows `fun IamANat ↦ Bool : ℕ → Type`
  logInfo <| Expr.lam `IamANat (Expr.const ``Nat []) (Expr.const ``Bool []) .default

hovering in the infoview above the IamANat displays fun IamANat ↦ Bool : ℕ → Type. I would have expected to see ℕ. Should I change my expectations?

Thanks!

[Damiano Testa]

(Maybe I should have mentioned that I am using VSCode.)

[Wojciech Nawrocki]

This is a bug in the delaborator (I think), try hovering over the binder in #check (λ (x : Nat) => x).

[Damiano Testa]

Wojciech, that's a much more minimal example, thanks!

Indeed, hovering on the x in fun x displays the whole function fun x ↦ x : ℕ → ℕ, while hovering on the second x just shows ℕ.