2 ms·
I believe you, but this hasn't been my experience. It took me hours to get Lean to work (something odd was happening with the package manager + version + toolin
by danilafe 5mo ago
I believe you, but this hasn't been my experience. It took me hours to get Lean to work (something odd was happening with the package manager + version + tooling combination). Agda worked out of the box with macOS homebrew. Agda's docs are petty bad, but I've found its cross-linked module documentation incredibly useful. The main issue is knowing something exists.
- fooker 5mo agoThis has also been my experience with lean4. I don't understand the forced vscode path, just let me get it as normal software in a convenient way and run it as a tool
- danilafe 5mo agoTo be fair, Coq has ProofGeneral and Agda has its emacs mode. Once you go outside these established channels, oftentimes using the tool becomes incredibly difficult. I guess for interactive theorem proving in general you may need some sort of editor at some point.
- JuniperMesos 5mo agoYeah, I'm not a fan of the encouragement to use vscode; that said it was pretty easy for me to get neovim set up with Lean tooling, and that's what I use generally.