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: upstream Std.Data.Nat #3634

Merged
merged 4 commits into from
Mar 8, 2024
Merged

chore: upstream Std.Data.Nat #3634

merged 4 commits into from
Mar 8, 2024

Conversation

joehendrix
Copy link
Contributor

@joehendrix joehendrix commented Mar 7, 2024 •
edited
Loading

This migrates lemmas about Nat compare, min, max, dvd, gcd, lcm and div/mod from Std to Lean itself.

Std still has some additional recursors, CoPrime and a few additional definitions that might merit further discussion prior to upstreaming.

@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc March 7, 2024 22:02 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, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

Mathlib CI status (docs):

  • ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 6af7a01af643e82e1deeb6b7523b8099d177b159 --onto 611b1746896bbadf459c00cc218fa31cf51b4e08. (2024-03-07 22:05:32)

@joehendrix joehendrix added will-merge-soon …unless someone speaks up and removed toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN labels Mar 8, 2024
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc March 8, 2024 16:06 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 8, 2024
@joehendrix joehendrix changed the title chore: upstream variety of lemmas about Nat from Init chore: upstream Std.Data.Nat Mar 8, 2024
@joehendrix joehendrix mentioned this pull request Mar 8, 2024
Merged
@joehendrix joehendrix added this pull request to the merge queue Mar 8, 2024
Merged via the queue into master with commit 6dd4f4b Mar 8, 2024
20 checks passed
github-merge-queue bot pushed a commit that referenced this pull request Mar 11, 2024
@joehendrix
chore: upstream Std.Data.Int (#3635)
c43a6b5 
This depends on #3634.
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
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
@joehendrix @leanprover-community-mathlib4-bot