Skip to content

feat: let simp simplify numerals #8433

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
Open
JovanGerb wants to merge 11 commits into
base: master
Choose a base branch
from
Open

feat: let simp simplify numerals #8433

JovanGerb wants to merge 11 commits into from

Conversation

@JovanGerb
Copy link
Contributor

@JovanGerb JovanGerb commented May 21, 2025 •
edited
Loading

This PR lets simp simplify the type and instance of number literals.

This came up here: leanprover-community/mathlib4#24492 (comment)

@JovanGerb JovanGerb requested a review from leodemoura as a code owner May 21, 2025 14:20
@JovanGerb JovanGerb marked this pull request as draft May 21, 2025 14:20
@JovanGerb JovanGerb mentioned this pull request May 21, 2025
Closed
@grunweg
Copy link
Contributor

grunweg commented May 21, 2025

(Would you like to add a test, at some point? I know this PR is still a draft.)

@JovanGerb JovanGerb changed the title feat: let simp and dsimp simplify numerals feat: let simp simplify numerals May 21, 2025
@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 22, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request May 22, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#8433
6807731
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request May 22, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#8433
f8e42db
@leanprover-community-bot leanprover-community-bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label May 22, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented May 22, 2025 •
edited
Loading

Mathlib CI status (docs):

@leanprover-community-bot leanprover-community-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 May 23, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request May 23, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#8433
12364c1
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request May 23, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#8433
dcced5f
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request May 24, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#8433
9d923be
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request May 24, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#8433
063ad40
@JovanGerb
Copy link
Contributor Author

JovanGerb commented May 24, 2025

I've added a test now, which is a minimization of the example in Mathlib.

@JovanGerb JovanGerb marked this pull request as ready for review May 24, 2025 15:36
@leanprover-bot leanprover-bot added the P-low We are not planning to work on this issue label May 28, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@leodemoura leodemoura Awaiting requested review from leodemoura leodemoura is a code owner

Assignees

No one assigned

Labels

builds-mathlib CI has verified that Mathlib builds against this PR P-low We are not planning to work on this issue 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.

4 participants

@JovanGerb @grunweg @leanprover-community-bot @leanprover-bot