Zulip Chat Archive

Stream: general

Topic: switching between extensions

Joseph O (May 03 2022 at 13:52):

In VSCode, I alternate between using lean and lean 4 (i use lean for theorem proving and lean 4 for more general-purpose things), and I find it really annoying to constantly disable one extension and enable the other when using different versions. Is there a better alternative?

Joseph O (May 03 2022 at 13:53):

Some VSCode hack i dont know of?

Last updated: Dec 20 2023 at 11:08 UTC