Zulip Chat Archive

Stream: general

Topic: How does lean work?

view this post on Zulip Ali Caglayan (Aug 02 2018 at 00:01):

I want to understand how lean works. I have tried playing with the command line however I can only compile lean files. I have played with the emacs mode and thats fine, however there is only one problem. I hate emacs.

I have past experience with Coq, in coq there is an interactive mode apart from the compiler coqc, called coqtop and ontop of that there is an ide called coqide which essentially is a gui coqtop.

What is the closest thing to any of these with lean?

view this post on Zulip Sebastian Ullrich (Aug 02 2018 at 00:23):

Emacs is the only available interactive frontend for Lean 2. For Lean 3 there is an official VS Code plugin.

view this post on Zulip Kevin Sullivan (Aug 02 2018 at 03:43):

I suggest using Visual Studio Code and the VS Code extension for Lean.

Last updated: May 18 2021 at 16:25 UTC