Fantastic. First time I saw something similar to this was Edwin Brady’s recent demo of Idris 2. It’s quite amazing just how much of a program can be machine-written when the types are strict enough.

I hope holes & case-splitting get into many more languages.