3 ms·

Thanks. I'd assumed idris2 would replace idris so I didn't try searching for anything else. I've just grabbed it, thanks very much for the tip.