Zulip Chat Archive

Stream: general

Topic: notation for the extension

Sebastien Gouezel (May 21 2021 at 15:00):

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 (May 21 2021 at 15:01):

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

Sebastien Gouezel (May 21 2021 at 15:08):

Done, thanks!

Last updated: Dec 20 2023 at 11:08 UTC