5 ms·

Actually doing in Agda first. Coinductive programming is a delight with Agda 2.5. But yes that's the plan.