Closed buzden closed 3 years ago
I'll merge this, although I think that usually small cosmetic changes don't merit their own PR.
I'll merge this, although I think that usually small cosmetic changes don't merit their own PR.
How do you suggest to suggest you such changes? Do you think they should go inside meaningful PRs, even if they'are unrelated semantically?
I think to just leave the code as it is, especially if we are talking just about personal taste / preferences without an agreed upon coding style. Reviewing PRs takes time and even minor changes always come with the risk of introducing regressions. So one has to weigh the benefits of one against the other.
See also the following part of the Idris2 contributing guidelines.
Please note that the above doesn't mean that there are no places in the code that actually do not require some cleanup. It's difficult to draw a line here, and I definitely don't want to scare you or other people away from further contributions. Your work is highly welcome. :-)
I personally find sections be more readable than explicit application, so what do you think?