5 ms·
Lean hits a really good middle ground I think. More resources for Agda probably. But I'm very fond of lean ;)
by cmrx64 9y ago
Lean hits a really good middle ground I think. More resources for Agda probably. But I'm very fond of lean ;)
- solomatov 9y agoLean is very interesting, but Agda and especially Coq has more learning resource, so for the beginners it's probably better to start from them, even though, in some sense Lean is more modern.
- evincarofautumn 9y agoI have the impression that for someone coming from a programming background, Idris is also a pretty good introduction to the world of dependently typed programming and proof assistants.