RFC: style: number of spaces before | #2580
Description
Proposal
I propose to make the amount of spaces used before \ consistent. Currently it is a mix of zero or two spaces, with a majority being two spaces. (There is very few places where another number such as 3 or 4 is used, I'll send a pr for that soon)
Other projects such as std and mathlib are doing two spaces.
- User Experience: How does this feature improve the user experience?
The user does not have to think how many spaces to type, automation tools can make consistent choices.
- Beneficiaries: Which Lean users and projects benefit most from this feature/change?
I suppose mainly those that write code in core lean, but of course this style, when done here, will probably be imitated by many other projects.
- Maintainability: Will this change streamline code maintenance or simplify its structure?
Probably it will minimally simplify maintenance.
Community Feedback
Ideas should be discussed on the Lean Zulip prior to submitting a proposal. Summarize all prior discussions and link them here.
Summary: Two spaces is the de-factor convention, so let's go with this.
Impact
Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.