[Merged by Bors] - chore: replace `λ` by `fun` #11301

grunweg · 2024-03-11T19:46:44Z

Per the style guidelines, λ is disallowed in mathlib.
This is close to exhaustive; I left some tactic code alone when it seemed to me that tactic could be upstreamed soon.

Notes

In lines I was modifying anyway, I also converted => to ↦.
Also contains some mild in-passing indentation fixes in Mathlib/Order/SupClosed.
Some doc comments still contained Lean 3 syntax λ x, , which I also replaced.

grunweg · 2024-03-11T20:09:36Z

Drive-by question: is the Lean 3 syntax used in comments in Data/FunLike/{Embedding,Equiv} and Data/Polynomial/Laurent intended, or did somebody simply forget to fix this during the port?

Mathlib/Algebra/Field/ULift.lean

Mathlib/Algebra/Group/ULift.lean

Mathlib/Analysis/SpecificLimits/Basic.lean

Mathlib/Combinatorics/Quiver/Cast.lean

Co-authored-by: Moritz Doll <moritz.doll@googlemail.com>

mcdoll

I am pretty sure that we don't want any Lean 3 syntax anymore in the comments.
I am less sure whether we want to ban λ from meta-code.

test/MfldSetTac.lean

After the fun keyword, also replace => by \mapsto.

grunweg · 2024-03-12T12:38:39Z

I'll be happy to drop the changes to the Lean/Meta or Tactic directory, if I hear this is desired.
The style guide says "The lambda notation λ x ↦ x * x, while syntactically valid, is disallowed in mathlib in favor of the fun keyword.", which to me seems to include any mathlib tactics. (If this is not desired, this should be updated: happy to make a PR.)

dupuisf · 2024-03-14T10:04:24Z

Thanks a lot!

bors r+

Per the style guidelines, `λ` is disallowed in mathlib. This is close to exhaustive; I left some tactic code alone when it seemed to me that tactic could be upstreamed soon. Notes - In lines I was modifying anyway, I also converted `=>` to `↦`. - Also contains some mild in-passing indentation fixes in `Mathlib/Order/SupClosed`. - Some doc comments still contained Lean 3 syntax `λ x, `, which I also replaced. <!-- The text above the `

mathlib-bors · 2024-03-14T11:12:17Z

Pull request successfully merged into master.

Build succeeded:

grunweg · 2024-03-14T14:08:01Z

@dupuisf Thank you for the review!
Can you help me interpret your 👍 on my comment, please? Did you mean

"I also had this question"
"I think the syntax is intential"
"I think somebody forgot about this; a PR is welcome"?
something else?

As a mathematician, I have a hard time interpreting a "yes" answer to an "or" question :-)

dupuisf · 2024-03-15T19:44:30Z

Sorry for being cryptic :-) I meant that I agree that the Lean 3 syntax in the comments is almost certainly an artifact of the port and should have been converted to Lean 4 syntax.

- lambda by fun (and "=>" by "\mapsto", while I was it) - remove commas after fields (there are seemingly allowed, but not necessary) - indent code per the style guide I did not consistently switch to `where` syntax; I was not sure if this has side effects (e.g. on performance). If desired, I can make that change also. I did not test the code samples; they might be broken (but at least their syntax works). Follow-up to #11301.

grunweg · 2024-03-15T20:59:38Z

Thanks for elaborating. I just looked into this; five PRs later, this has been fixed. #11405 and #11409 are particular off-spring.

Includes some doc comments and real code: this is exhaustive, with two exceptions: - some files are handled in #11409 instead - I left FunProp/{ToStd,RefinedDiscTree}.lean, Tactic/NormNum and Tactic/Simps alone, as these seem likely enough to end up in std. Follow-up to #11301, much shorter this time.

@Vierkantor

Fully update the module docstrings (in particular, the examples given therein) after #8386. This includes switching to where syntax, but also replacing Lean 3 syntax, replacing => by "\mapsto" while at it and indenting code per the style guide. As such, it's also a follow-up to #11301. Co-authored-by: @Vierkantor Co-authored-by: Vierkantor <vierkantor@vierkantor.com>

Per the style guidelines, `λ` is disallowed in mathlib. This is close to exhaustive; I left some tactic code alone when it seemed to me that tactic could be upstreamed soon. Notes - In lines I was modifying anyway, I also converted `=>` to `↦`. - Also contains some mild in-passing indentation fixes in `Mathlib/Order/SupClosed`. - Some doc comments still contained Lean 3 syntax `λ x, `, which I also replaced. <!-- The text above the `

Includes some doc comments and real code: this is exhaustive, with two exceptions: - some files are handled in #11409 instead - I left FunProp/{ToStd,RefinedDiscTree}.lean, Tactic/NormNum and Tactic/Simps alone, as these seem likely enough to end up in std. Follow-up to #11301, much shorter this time.

@Vierkantor

Fully update the module docstrings (in particular, the examples given therein) after #8386. This includes switching to where syntax, but also replacing Lean 3 syntax, replacing => by "\mapsto" while at it and indenting code per the style guide. As such, it's also a follow-up to #11301. Co-authored-by: @Vierkantor Co-authored-by: Vierkantor <vierkantor@vierkantor.com>

Per the style guidelines, `λ` is disallowed in mathlib. This is close to exhaustive; I left some tactic code alone when it seemed to me that tactic could be upstreamed soon. Notes - In lines I was modifying anyway, I also converted `=>` to `↦`. - Also contains some mild in-passing indentation fixes in `Mathlib/Order/SupClosed`. - Some doc comments still contained Lean 3 syntax `λ x, `, which I also replaced. <!-- The text above the `

Includes some doc comments and real code: this is exhaustive, with two exceptions: - some files are handled in #11409 instead - I left FunProp/{ToStd,RefinedDiscTree}.lean, Tactic/NormNum and Tactic/Simps alone, as these seem likely enough to end up in std. Follow-up to #11301, much shorter this time.

@Vierkantor

Fully update the module docstrings (in particular, the examples given therein) after #8386. This includes switching to where syntax, but also replacing Lean 3 syntax, replacing => by "\mapsto" while at it and indenting code per the style guide. As such, it's also a follow-up to #11301. Co-authored-by: @Vierkantor Co-authored-by: Vierkantor <vierkantor@vierkantor.com>

Per the style guidelines, `λ` is disallowed in mathlib. This is close to exhaustive; I left some tactic code alone when it seemed to me that tactic could be upstreamed soon. Notes - In lines I was modifying anyway, I also converted `=>` to `↦`. - Also contains some mild in-passing indentation fixes in `Mathlib/Order/SupClosed`. - Some doc comments still contained Lean 3 syntax `λ x, `, which I also replaced. <!-- The text above the `

Includes some doc comments and real code: this is exhaustive, with two exceptions: - some files are handled in #11409 instead - I left FunProp/{ToStd,RefinedDiscTree}.lean, Tactic/NormNum and Tactic/Simps alone, as these seem likely enough to end up in std. Follow-up to #11301, much shorter this time.

@Vierkantor

Fully update the module docstrings (in particular, the examples given therein) after #8386. This includes switching to where syntax, but also replacing Lean 3 syntax, replacing => by "\mapsto" while at it and indenting code per the style guide. As such, it's also a follow-up to #11301. Co-authored-by: @Vierkantor Co-authored-by: Vierkantor <vierkantor@vierkantor.com>

Includes some doc comments and real code: this is exhaustive, with two exceptions: - some files are handled in #11409 instead - I left FunProp/{ToStd,RefinedDiscTree}.lean, Tactic/NormNum and Tactic/Simps alone, as these seem likely enough to end up in std. Follow-up to #11301, much shorter this time.

@Vierkantor

Fully update the module docstrings (in particular, the examples given therein) after #8386. This includes switching to where syntax, but also replacing Lean 3 syntax, replacing => by "\mapsto" while at it and indenting code per the style guide. As such, it's also a follow-up to #11301. Co-authored-by: @Vierkantor Co-authored-by: Vierkantor <vierkantor@vierkantor.com>

Per the style guidelines, `λ` is disallowed in mathlib. This is close to exhaustive; I left some tactic code alone when it seemed to me that tactic could be upstreamed soon. Notes - In lines I was modifying anyway, I also converted `=>` to `↦`. - Also contains some mild in-passing indentation fixes in `Mathlib/Order/SupClosed`. - Some doc comments still contained Lean 3 syntax `λ x, `, which I also replaced. <!-- The text above the `

Includes some doc comments and real code: this is exhaustive, with two exceptions: - some files are handled in #11409 instead - I left FunProp/{ToStd,RefinedDiscTree}.lean, Tactic/NormNum and Tactic/Simps alone, as these seem likely enough to end up in std. Follow-up to #11301, much shorter this time.

@Vierkantor

Fully update the module docstrings (in particular, the examples given therein) after #8386. This includes switching to where syntax, but also replacing Lean 3 syntax, replacing => by "\mapsto" while at it and indenting code per the style guide. As such, it's also a follow-up to #11301. Co-authored-by: @Vierkantor Co-authored-by: Vierkantor <vierkantor@vierkantor.com>

Per the style guidelines, `λ` is disallowed in mathlib. This is close to exhaustive; I left some tactic code alone when it seemed to me that tactic could be upstreamed soon. Notes - In lines I was modifying anyway, I also converted `=>` to `↦`. - Also contains some mild in-passing indentation fixes in `Mathlib/Order/SupClosed`. - Some doc comments still contained Lean 3 syntax `λ x, `, which I also replaced. <!-- The text above the `

Includes some doc comments and real code: this is exhaustive, with two exceptions: - some files are handled in #11409 instead - I left FunProp/{ToStd,RefinedDiscTree}.lean, Tactic/NormNum and Tactic/Simps alone, as these seem likely enough to end up in std. Follow-up to #11301, much shorter this time.

@Vierkantor

Fully update the module docstrings (in particular, the examples given therein) after #8386. This includes switching to where syntax, but also replacing Lean 3 syntax, replacing => by "\mapsto" while at it and indenting code per the style guide. As such, it's also a follow-up to #11301. Co-authored-by: @Vierkantor Co-authored-by: Vierkantor <vierkantor@vierkantor.com>

grunweg added awaiting-review awaiting-CI labels Mar 11, 2024

grunweg added 2 commits March 11, 2024 21:07

Replace some \lambda by fun: initial batch of changes.

79c5d0b

Fix occurrences in test/Simps.lean.

4788e74

grunweg force-pushed the MR-lambda-fun branch 2 times, most recently from d93ec60 to 466480d Compare March 11, 2024 20:52

github-actions bot removed the awaiting-CI label Mar 11, 2024

Fixup.

4a84760

grunweg force-pushed the MR-lambda-fun branch from 466480d to 4a84760 Compare March 11, 2024 21:42

mcdoll reviewed Mar 11, 2024

View reviewed changes

grunweg and others added 2 commits March 12, 2024 08:40

Apply suggestions from code review

3336ae5

Co-authored-by: Moritz Doll <moritz.doll@googlemail.com>

Follow-up.

3e7eaf1

mcdoll reviewed Mar 12, 2024

View reviewed changes

test/MfldSetTac.lean Outdated Show resolved Hide resolved

grunweg added 2 commits March 12, 2024 13:29

Replace "\mapsto " by "\mapsto ", i.e. remove double spaces.

32728bf

Replace some double space after =>.

aa85247

After the fun keyword, also replace => by \mapsto.

github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Mar 14, 2024

mathlib-bors bot changed the title ~~chore: replace λ by fun~~ [Merged by Bors] - chore: replace λ by fun Mar 14, 2024

mathlib-bors bot closed this Mar 14, 2024

mathlib-bors bot deleted the MR-lambda-fun branch March 14, 2024 11:12

grunweg mentioned this pull request Mar 15, 2024

[Merged by Bors] - chore: replace remaining lambda syntax #11405

Closed

grunweg mentioned this pull request Mar 15, 2024

[Merged by Bors] - chore(Data/Funlike): update examples and replace Lean 3 syntax #11409

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - chore: replace `λ` by `fun` #11301

[Merged by Bors] - chore: replace `λ` by `fun` #11301

grunweg commented Mar 11, 2024 •

edited

Loading

grunweg commented Mar 11, 2024

mcdoll left a comment

grunweg commented Mar 12, 2024

dupuisf commented Mar 14, 2024

mathlib-bors bot commented Mar 14, 2024

grunweg commented Mar 14, 2024

dupuisf commented Mar 15, 2024

grunweg commented Mar 15, 2024

[Merged by Bors] - chore: replace λ by fun #11301

[Merged by Bors] - chore: replace λ by fun #11301

Conversation

grunweg commented Mar 11, 2024 • edited Loading

grunweg commented Mar 11, 2024

mcdoll left a comment

Choose a reason for hiding this comment

grunweg commented Mar 12, 2024

dupuisf commented Mar 14, 2024

mathlib-bors bot commented Mar 14, 2024

grunweg commented Mar 14, 2024

dupuisf commented Mar 15, 2024

grunweg commented Mar 15, 2024

[Merged by Bors] - chore: replace `λ` by `fun` #11301

[Merged by Bors] - chore: replace `λ` by `fun` #11301

grunweg commented Mar 11, 2024 •

edited

Loading