notation for the extension

Stream: general

[Sebastien Gouezel]

I'd like to add the following notation to the vscode extension:

    "ennreal" : "ℝ≥0∞",

However, I don't know to which project I should make a PR (are there two separate projects for lean 3 and lean 4 or have they been merged? Should I make a PR to both of them if they haven't?)

[Gabriel Ebner]

The PR should go to vscode-lean (the Lean 3), I'll merge it manually to the Lean 4 one.

[Sebastien Gouezel]

Done, thanks!