[tom_mellior]

Out of interest, what about this tutorial do you find better than (which?) Coq tutorials?

I think Lean might be the better technology, but I don't think this tutorial is better than Software Foundations. I can't see beginners not being turned off by boring discussions of hierarchies of universes before the first real proofs to get you hooked.

[benwr]

This tutorial starts by explaining how things work, and only later shows you magic. That's exactly what I like about it, actually. Almost every coq tutorial I found (I tried software foundations, cpdt, and several shorter online tutorials) fails to explain what you're doing before you do it.

[tom_mellior]

Fair enough. That's not my preferred approach to tutorials, but tastes differ. Thanks.