alt Hacker NewsI've used agda a tiny bit and Lean somewhat more, and I definitely found it much easier to write functional programs not focused on mathematical proofs in Lean than Agda. IIRC the difference was mostly tooling - Agda's documentation is kind of bad and it's a pain to get it working on your system (and it really wants you to be using Emacs specifically). Whereas Lean documents how to write the cat utility in its own docs and generally has a much better, more modern tooling experience.
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.