Rain 🚱 is a user on cybre.space. You can follow them or interact with them if you have an account anywhere in the fediverse.
> This means that, for instance, every Vect will take O(n^2) space due to the unary Nats, and similar problems will obtain for many other types.
https://github.com/idris-lang/Idris-dev/issues/3149
*sigh*
