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

chore: remove @[simp] from bind_eq_some #4314

Merged
merged 1 commit into from
Jun 1, 2024
Merged

chore: remove @[simp] from bind_eq_some #4314

merged 1 commit into from
Jun 1, 2024

Conversation

semorrison
Copy link
Collaborator

No description provided.

@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc May 31, 2024 15:28 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 May 31, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request May 31, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#4314
0d26462
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request May 31, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#4314
e789b74
semorrison added a commit to leanprover-community/mathlib4 that referenced this pull request May 31, 2024
@semorrison
fixes for leanprover/lean4#4314
3f23ed2
@leanprover-community-mathlib4-bot
Copy link
Collaborator

leanprover-community-mathlib4-bot commented May 31, 2024 •
edited
Loading

Mathlib CI status (docs):

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan release-ci Enable all CI checks for a PR, like is done for releases labels May 31, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request May 31, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#4314
5ffd643
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request May 31, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#4314
ace059b
@semorrison
Copy link
Collaborator Author

I have the Mathlib fixes, but on an apparently-inaccessible-via-ssh machine right now. I'll finish this once I'm home next week.

@semorrison semorrison added this pull request to the merge queue Jun 1, 2024
Merged via the queue into master with commit 299cb9a Jun 1, 2024
26 checks passed
@semorrison semorrison mentioned this pull request Jun 4, 2024
Closed
mathlib-bors bot pushed a commit to leanprover-community/mathlib4 that referenced this pull request Jun 4, 2024
@semorrison
chore: adaptations for nightly-2024-06-02 (#13491)
2d3147b 
Changes required for leanprover/lean4#4314 and leanprover/lean4#4179.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan release-ci Enable all CI checks for a PR, like is done for releases 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.

None yet
2 participants
@semorrison @leanprover-community-mathlib4-bot