| Big: * tactics (proof scripts are a lot easier than manual proving) * syntax extensibility (Racket-like, supports custom elaboration/delaboration) * mathlib (library of formalized math) * 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) |
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.