[Merged by Bors] - style: fix some mis-placed by#13203
[Merged by Bors] - style: fix some mis-placed by#13203
Conversation
This fixes the worst cases, where the 'by' was not even indented correctly.
Ruben-VandeVelde
left a comment
There was a problem hiding this comment.
You're allowed to argue I'm scope-creeping your PR :)
| example (x : ℝ) : deriv (fun x ↦ cos (sin x) * exp x) x = (cos(sin(x))-sin(sin(x))*cos(x))*exp(x) := | ||
| by { simp, ring } | ||
| example (x : ℝ) : | ||
| deriv (fun x ↦ cos (sin x) * exp x) x = (cos(sin(x))-sin(sin(x))*cos(x))*exp(x) := by |
There was a problem hiding this comment.
I'm not even sure the over-parenthesized syntax works in lean 4
There was a problem hiding this comment.
Trying on the playground: This syntax parses, without the spaces it does not. It seems the example fails, though...
You are, but that need not be a problem :-) If you test and suggest a change, I'm happy to accept it - I am less willing to do this legwork myself. To this end, I have just accepted all of your suggestions, except for one which needs checking. |
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
grunweg
left a comment
There was a problem hiding this comment.
Good catch on all of them, thanks!
|
✌️ grunweg can now approve this pull request. To approve and merge a pull request, simply reply with |
|
Thanks for the review; I followed your suggestion. |
|
Pull request successfully merged into master. Build succeeded: |
Commits can be reviewed individually: the second commit is fully automatic (using VS Code's search-and-replace, in regex mode); the last commit fixes the line length (updating the syntax of that comment to Lean 4).