Zulip Chat Archive

Stream: lean4

Topic: editors for Lean 4


mario jose (Nov 29 2021 at 02:57):

what is the best text editor to use lean 4?
i am gonna start to learn lean 4 as my first proof assistant language

mario jose (Nov 29 2021 at 02:58):

I mean what text editors have good plugins for lean 4

Scott Morrison (Nov 29 2021 at 03:01):

Most people are using VS Code, with the Lean 4 plugin.

Scott Morrison (Nov 29 2021 at 03:01):

There is an emacs mode as well.

Scott Morrison (Nov 29 2021 at 03:02):

Start reading at https://leanprover.github.io/lean4/doc/setup.html

Scott Morrison (Nov 29 2021 at 03:02):

(You may find that Lean 3 is an easier place to start: Lean 4 is not particularly beginner friendly yet.)

mario jose (Nov 29 2021 at 03:13):

is the difference between programming on lean 4 and lean 3 noticeable in regards to syntax?

Scott Morrison (Nov 29 2021 at 04:04):

Yes.


Last updated: Dec 20 2023 at 11:08 UTC