4 ms·

I have good results from having a default prompt that instructs using Idris with indexed/dependent types ,(without that the bravest it gets is GADTs)