refactor(*): remove unnecessary uses of λ
#3935
Conversation
the expression (- x) is interpreted as the unary minus, instead of a partially applied binary minus
fpvandoorn
added
the
awaiting-review
There was a problem hiding this comment.
LGTM.
In addition to the changes removing redundant lambdas, there are some changes that change whitespace, add/remove parens, and shorten expressions with dot notation (see e.g. src/tactic/omega/coeffs.lean). They all seem uncontroversial.
This touches many files, so would be good to get merged quickly.
| ∧ (∀ (m : ℕ), (m : with_top ℕ) < n → | ||
| differentiable_on 𝕜 (λ x, iterated_fderiv_within 𝕜 m f s x) s) := | ||
| differentiable_on 𝕜 ((iterated_fderiv_within 𝕜 m f s)) s) := |
There was a problem hiding this comment.
are the extra parens necessary? (I'm guessing they're autogenerated?)
There was a problem hiding this comment.
(the same comment applies to the next few lines of the same file. I didn't see potentially-redundant parentheses anywhere else.)
|
I'm sure I can eventually get used to this, but this surely hurts readability for the "curious mathematician". The difference between |
|
Why are we doing this? |
|
The double parentheses are search+replace mistakes. |
|
I'm also not sure about all of these changes. Some of the eta reductions look reasonable. But when infix notation is involved, the lambda version seems much clearer. Not only for beginners, even for me. Is there an advantage to the change that I'm missing? |
fpvandoorn
removed
the
awaiting-review
|
Ok, that's fair. I'll close this PR. If we consistently want to use a certain notation, I might open a new PR. |
Most changes are of the form
(λ x, x + c)->(+ c)and(λ x, c + x)->((+) c)(and also for*,/,<,≤, etc)It doesn't work for
-, since neither(- x)and((-) x)are parser correctly (presumably because of the unary minusThe shorter version also sometimes doesn't work if coercions are inserted.