Zulip Chat Archive

Stream: general

Topic: How does lean work?

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?

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.

Kevin Sullivan (Aug 02 2018 at 03:43):

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

Last updated: Dec 20 2023 at 11:08 UTC