How does lean work?

Stream: general

[Ali Caglayan]

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]

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

[Kevin Sullivan]

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