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: tree map lemmas for modify #7379

Closed
wants to merge 3 commits into from
Closed

feat: tree map lemmas for modify #7379

wants to merge 3 commits into from

Conversation

datokrat
Copy link
Contributor

@datokrat datokrat commented Mar 7, 2025

This PR provides lemmas about the tree map function modify and its interactions with other functions for which lemmas already exist.

@datokrat datokrat added the changelog-library Library label Mar 7, 2025
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc March 7, 2025 11:38 Inactive
@datokrat datokrat force-pushed the paul/treemaplemmas13 branch from aa5b3a4 to 9f17f88 Compare March 7, 2025 11:39
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc March 7, 2025 11:42 Inactive
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Mar 7, 2025
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

  • ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2025-03-07 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-07 12:05:08)

@datokrat datokrat marked this pull request as ready for review March 7, 2025 12:43
@datokrat datokrat requested a review from TwoFX as a code owner March 7, 2025 12:43
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc March 10, 2025 09:20 Inactive
@datokrat datokrat force-pushed the paul/treemaplemmas13 branch from ae92422 to 83da7ac Compare March 10, 2025 11:07
@datokrat datokrat changed the base branch from paul/treemaplemmas12 to master March 10, 2025 11:07
@datokrat datokrat enabled auto-merge March 10, 2025 11:08
@datokrat datokrat disabled auto-merge March 10, 2025 12:41
@datokrat
Copy link
Contributor Author

(Sorry for falsely requesting a review from you all... Because I temporarily had the wrong base branch after a rebase, the PR temporarily contained many commits from master, and GitHub consequently requested reviews from the respective code owners. There's nothing you need to review in here.)

@datokrat datokrat closed this Mar 10, 2025
@datokrat datokrat mentioned this pull request Mar 10, 2025
Merged
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc March 10, 2025 13:09 Inactive
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@TwoFX TwoFX TwoFX approved these changes

Assignees
No one assigned
Labels
changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@datokrat @leanprover-community-bot @TwoFX