Idris2 Playground for learning how dependent types work