I need to add extensible quality instances for a new development in rewrite rules. It is however easy to isolate, even if currently useless.
Should I make it a PR or wait and include it to that new development ?
please explain more why you need it
I am going to spawn many new quality variables, and it's dealt with the same way as when there are more universes than given in the univdecl. I don't strictly need it this way, but this would fit and I don't see why it would hurt the rest of the codebase
no need for separate PR I think
Last updated: Oct 13 2024 at 01:02 UTC