[Merged by Bors] - chore(Data/Funlike): update examples and replace Lean 3 syntax#11409
Closed
[Merged by Bors] - chore(Data/Funlike): update examples and replace Lean 3 syntax#11409
Conversation
- 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.
This was referenced Mar 15, 2024
grunweg
commented
Mar 15, 2024
grunweg
commented
Mar 15, 2024
Contributor
|
Here, there is an additional issue: the whole |
mathlib-bors bot
pushed a commit
that referenced
this pull request
Mar 17, 2024
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.
Contributor
|
Thank you for letting me know, I totally forgot about updating the |
Contributor
Author
|
Thank you for the thorough update! I have just merged master and updated the PR description. |
mathlib-bors bot
pushed a commit
that referenced
this pull request
Mar 20, 2024
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>
Contributor
|
Pull request successfully merged into master. Build succeeded: |
dagurtomas
pushed a commit
that referenced
this pull request
Mar 22, 2024
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.
dagurtomas
pushed a commit
that referenced
this pull request
Mar 22, 2024
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>
utensil
pushed a commit
that referenced
this pull request
Mar 26, 2024
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.
utensil
pushed a commit
that referenced
this pull request
Mar 26, 2024
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>
xgenereux
pushed a commit
that referenced
this pull request
Apr 15, 2024
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.
xgenereux
pushed a commit
that referenced
this pull request
Apr 15, 2024
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>
atarnoam
pushed a commit
that referenced
this pull request
Apr 16, 2024
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.
atarnoam
pushed a commit
that referenced
this pull request
Apr 16, 2024
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>
uniwuni
pushed a commit
that referenced
this pull request
Apr 19, 2024
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.
uniwuni
pushed a commit
that referenced
this pull request
Apr 19, 2024
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>
callesonne
pushed a commit
that referenced
this pull request
Apr 22, 2024
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.
callesonne
pushed a commit
that referenced
this pull request
Apr 22, 2024
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>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
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