Skip to content

feat: verification of Nat.toDigits, Nat.repr and ToString Nat#12445

Open
datokrat wants to merge 3 commits intomasterfrom
paul/todigits
Open

feat: verification of Nat.toDigits, Nat.repr and ToString Nat#12445
datokrat wants to merge 3 commits intomasterfrom
paul/todigits

Conversation

@datokrat
Copy link
Contributor

@datokrat datokrat commented Feb 11, 2026

This PR provides lemmas characterizing Nat.toDigits, Nat.repr and ToString Nat.

@datokrat datokrat added the changelog-library Library label Feb 11, 2026
@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 Feb 11, 2026
@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Feb 11, 2026

Reference manual CI status:

  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-02-10 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-02-11 19:59:56)

mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Feb 11, 2026
Update lean-toolchain for testing leanprover/lean4#12445
5c7e049
@github-actions github-actions bot added the mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN label Feb 11, 2026
mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Feb 11, 2026
Update lean-toolchain for testing leanprover/lean4#12445
9c7ee53
@mathlib-lean-pr-testing mathlib-lean-pr-testing bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Feb 11, 2026
@mathlib-lean-pr-testing
Copy link

mathlib-lean-pr-testing bot commented Feb 11, 2026

Mathlib CI status (docs):

mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Feb 12, 2026
Update lean-toolchain for leanprover/lean4#12445
8801490
mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Feb 12, 2026
Update lean-toolchain for leanprover/lean4#12445
bdac4fd
@mathlib-lean-pr-testing mathlib-lean-pr-testing 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 Feb 12, 2026
@mathlib-lean-pr-testing
Copy link

mathlib-lean-pr-testing bot commented Feb 12, 2026

Mathlib CI status (docs):

@datokrat datokrat marked this pull request as ready for review February 13, 2026 19:39
@datokrat datokrat requested a review from kim-em as a code owner February 13, 2026 19:39
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@kim-em kim-em Awaiting requested review from kim-em kim-em is a code owner

Assignees

No one assigned

Labels

builds-mathlib CI has verified that Mathlib builds against this PR changelog-library Library mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN 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.

2 participants

@datokrat @leanprover-bot