lean4 icon indicating copy to clipboard operation
lean4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover

chore: indentation before `|`

Open mo271 opened this issue 2 years ago • 0 comments

This fixes indentation before | in places where the amount of spaces was not 0 or 2.

I suppose this is the non-controversial part of #2580. Deciding for either 0 or 2 to make it consistent would be a much larger change.

  • [X] Put an X in this bracket to confirm you have read the External Contribution Guidelines.

  • Please put the link to your RFC or bug issue here. PRs missing this link will be marked as missing RFC. #2580

mo271 avatar Sep 25 '23 15:09 mo271