RFC: style: number of spaces before |

[mo271]

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.

https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/style.20for.20proofs.20with.20.60.7C.60.2E

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.

[nomeata]

This is only about definitions defined by | clauses, but not about the match statement, where the clauses continue to be not indented relative to the match, correct?

[mo271]

yes, when there is a match the | should have the same indentation. There are a few handful of cases currently in the library where this is not the case, including an odd number of spaces perhaps also worth cleaning up.

[Kha]

Thanks for the RFC. As we do not have a formal style guide nor a code formatter implementing one nor do we want to create/review pure style changes manually, this RFC is not directly actionable. Thus I am closing it for the time being.