3 ms·

I'm planning to learn Agda for this very reason. Have you looked at Agda or other proof checkers? What about Lean made you decide to use it for this project? T

• outlace 7y ago
  Yes I've played with Agda before Lean. I found documentation for Agda to be sparse, maybe it's improved since then. Also, it was kind of a pain to get it setup. Lean was extremely easy to get running, works beautifully with VSCode, has great documentation and a helpful community. It's a "sexy" language and set of tooling compared to Agda and Coq (and I'm of the opinion aesthetics matter). It also feels more well-supported with the backing of Microsoft Research behind it.