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

refactor: state WellFoundedRelation Nat using <, not Nat.lt #5012

Merged
merged 1 commit into from
Aug 13, 2024
Merged

refactor: state WellFoundedRelation Nat using <, not Nat.lt #5012

merged 1 commit into from
Aug 13, 2024

Conversation

nomeata
Copy link
Collaborator

@nomeata nomeata commented Aug 13, 2024

as that’s the simp normal form.

@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 Aug 13, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Aug 13, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#5012
c4a53d0
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Aug 13, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#5012
63da718
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc August 13, 2024 11:34 Inactive
@nomeata nomeata changed the title refactor: state WellFoundedRelation Nat using <, not Nat.lt refactor: state WellFoundedRelation Nat using <, not Nat.lt Aug 13, 2024
@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 Aug 13, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

leanprover-community-mathlib4-bot commented Aug 13, 2024 •
edited
Loading

Mathlib CI status (docs):

nomeata added a commit to leanprover-community/mathlib4 that referenced this pull request Aug 13, 2024
@nomeata
Fix batteries branch pin (leanprover/lean4#5012)
b32f911
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Aug 13, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#5012
169bf39
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Aug 13, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#5012
4f66fb5
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Aug 13, 2024
@nomeata nomeata added the will-merge-soon …unless someone speaks up label Aug 13, 2024
@nomeata nomeata marked this pull request as ready for review August 13, 2024 13:37
@nomeata nomeata added this pull request to the merge queue Aug 13, 2024
Merged via the queue into master with commit 861ef27 Aug 13, 2024
33 checks passed
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
builds-mathlib CI has verified that Mathlib builds against this PR 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 will-merge-soon …unless someone speaks up
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@nomeata @leanprover-community-mathlib4-bot