Skip to content

fix: overeager Nat.sub constant folding #11043

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
Merged
hargoniX merged 2 commits into from
Nov 1, 2025
Merged

fix: overeager Nat.sub constant folding #11043

hargoniX merged 2 commits into from
Nov 1, 2025

Conversation

@Rob23oba
Copy link
Contributor

@Rob23oba Rob23oba commented Nov 1, 2025 •
edited
Loading

This PR fixes a case of overeager constant folding on Nat where the compiler would mistakenly assume 0 - x = x (see also #11042 for the same bug on UInts).

@github-actions github-actions bot added the changelog-compiler Compiler, runtime, and FFI label Nov 1, 2025
@Rob23oba Rob23oba marked this pull request as ready for review November 1, 2025 09:53
@hargoniX hargoniX added this pull request to the merge queue Nov 1, 2025
Merged via the queue into leanprover:master with commit 1fa67d0 Nov 1, 2025
17 checks passed
@Rob23oba Rob23oba deleted the nat-sub-fold branch November 1, 2025 10:34
@hargoniX hargoniX mentioned this pull request Nov 1, 2025
Merged
github-merge-queue bot pushed a commit that referenced this pull request Nov 1, 2025
@hargoniX
refactor: make constant folding more robust for future bugs (#11044)
3d30792 
This PR enforces users of the constant folder API to provide proofs of
their algebraic properties,
thus hopefully avoiding bugs such as #11042 and #11043 in the future.
@nomeata nomeata mentioned this pull request Nov 3, 2025
Closed
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

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

Assignees

No one assigned

Labels

changelog-compiler Compiler, runtime, and FFI

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@Rob23oba @hargoniX