Agda is nice and this tutorial is actually pretty great imho. I, for some reason, cannot stand when languages are not self hosting (that's my bug though; i'm no

Agda is nice and this tutorial is actually pretty great imho. I, for some reason, cannot stand when languages are not self hosting (that's my bug though; i'm not saying it's better or worse in general), so for me Idris 2 won out as dependently typed language I use for some proof work.