Hover information for definitions using parameters is misleading

[eric-wieser]

Hovering over the Gᵣ in the first #check Gᵣ in this code suggests that G is an explicit argument, even though #check tells me it is implicit.

import group_theory.subgroup
import data.int.cast

section

parameters {G : Type*} [ring G]

parameters (G)

def Gᵣ (r : ℤ) : add_subgroup G := add_subgroup.closure {r}



#check Gᵣ  -- Gᵣ : ℤ → add_subgroup G

end

#check Gᵣ -- Gᵣ : Π (G : Type u_1) [_inst_1 : ring G], ℤ → add_subgroup G

[gebner]

This is a bug in core Lean, the vscode extension is just printing what it gets from the server. And I fear it will stay this way for eternity. Lean 3 development has effectively ceased, and parameters were deprecated anyhow.

[eric-wieser]

This only came up because some of my old code I was trying to upgrade used parameters, and I couldn't work out why vscode was telling me the wrong thing. I guess I'll just try to strip them out entirely