3 ms·
I think CoqIDE is great and ProofGeneral (Emacs) is something all Coq experts use. I have the opposite experience with Lean 4, the VSCode integration is horrid
by sadfev 5y ago
I think CoqIDE is great and ProofGeneral (Emacs) is something all Coq experts use.
I have the opposite experience with Lean 4, the VSCode integration is horrid and documentation is awful.
The only good sources are papers for Lean4.
Granted I can go back to Lean3 but why would I?
- outlace 5y agoBut Lean4 is in alpha stage and there are no official stable releases yet, of course it's not well-documented nor polished yet. Lean3 works perfectly well and has everything you need.