* tooling (can't say it's better, I haven't used Idris, but it's at least a lot nicer than Agda's: rustup-like version manager `elan`, own build system `lake`, official vscode extension supporting mini web apps which can interact with the code)
Small things I can remember:
* do-notation with early return and imperative loops
* easier termination proof handling (provide some expression using function arguments with `decreasing_by` and prove it's decreasing with `termination_by` block, which may be automatic even for non-structural recursion because of some built-in tactic)
Regarding tactics: I started with Coq and I felt for a long time that I had no idea what tactics actually do. Proofs with tactics look nice on the surface, but I really did not like hidden state and hidden actions.
Redoing some proofs in Lean by construction of proof terms was eye-opening, it's just functional programming with dependent types! I still think that teaching with tactics first without exposing proof terms is a mistake.
I've learned to see the value of tactics later, again thanks to Lean: there are proofs that are more natural in the tactics style. Sometimes a mixed approach is ideal: growing intermediate proof terms from the premises and then wrangling the hypothesis with tactics to meet the lemmas.
Lean occupies a different point in the design space. Its type theory is simpler and more conservative, its metaprogramming system is more reminiscent of Racket's (including hygienic procedural macros), and the focus on supporting professional mathematicians gives a different feel to the community and libraries. I think both are worth knowing, but either is great to learn. I hope the two projects learn more from each other in the future.
