Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

feat: Add String.length_join and List.length_join #779

Open
wants to merge 2 commits into
base: main
Choose a base branch
from
Open

feat: Add String.length_join and List.length_join #779

wants to merge 2 commits into from

Conversation

tjf801
Copy link
Contributor

@tjf801 tjf801 commented May 3, 2024

Quick fix for #770.

@tjf801
Copy link
Contributor Author

tjf801 commented May 3, 2024

awaiting-review

@github-actions github-actions bot added the awaiting-review This PR is ready for review; the author thinks it is ready to be merged. label May 3, 2024
@tjf801 tjf801 mentioned this pull request May 3, 2024
Merged
digama0
digama0 reviewed May 3, 2024
View reviewed changes
Std/Data/List/Lemmas.lean Outdated
@@ -5,6 +5,7 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, M
-/
import Std.Control.ForInStep.Lemmas
import Std.Data.List.Basic
import Std.Data.Nat
Copy link
Member

@digama0 digama0 May 3, 2024 •
edited

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is a cross cutting import, and also not a precise import. The needed theorem(s) should move to Std.Data.Nat.Init.Lemmas and that should be imported here. If you only need the definition then it can just be an import of Std.Data.Nat.Basic.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is it possible to move the needed lemmas up into an Init folder, to reduce the imports needed here?

@urkud
Copy link
Member

urkud commented May 4, 2024 •
edited

Note that Mathlib has https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/BigOperators/List/Basic.html#List.length_join stated in terms of a generic List.sum instead of Nat.sum. What's the migration plan?

@semorrison
Copy link
Collaborator

Given that mathlib already has a List.length_join, we'll need to have a PR for mathlib that uses this branch of Std ready to go before this can be merged.

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label May 7, 2024
@tjf801 tjf801 changed the title Add String.length_join and List.length_join feat: Add String.length_join and List.length_join May 18, 2024
@tjf801 tjf801 changed the title feat: Add String.length_join and List.length_join feat: Add String.length_join and List.length_join May 18, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@semorrison semorrison semorrison left review comments

@digama0 digama0 digama0 left review comments

Assignees
No one assigned
Labels
awaiting-review This PR is ready for review; the author thinks it is ready to be merged. merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
5 participants
@tjf801 @urkud @semorrison @digama0 @leanprover-community-mathlib4-bot