fix: ignore no_index around OfNat.ofNat in norm_cast
#6438
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
|
This should fix the build error in leanprover-community/mathlib4#20169 |
github-actions
bot
added
the
toolchain-available
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
Dec 24, 2024
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Dec 24, 2024
leanprover-community-bot
added
the
builds-mathlib
|
Mathlib CI status (docs):
|
This was referenced Dec 28, 2024
mathlib-bors bot
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Jan 1, 2025
`ofNat(n)` is a shorthand for `no_index (OfNat.ofNat n)`. Its purpose is: * To make it easier to remember to write the `no_index` * To add a place to put a hoverable docstrings explaining the complexities * To make it easier to remove the `no_index`es in future if `DiscrTree`s stops needing them around `ofNat` (leanprover/lean4#2867). This is not exhaustive, but is a step in the right direction. For now, I only target (some of) the declarations with a `See note [no_index around OfNat.ofNat]`. Some theorem statements have been corrected in passing. This exposed two Lean bugs relating to not using `Expr.consumeMData`: * leanprover/lean4#6438 * leanprover/lean4#6467 These are made more likely by this PR adding `no_index` to the RHS of equalities, but were already possible to trigger by using `simp [<- _]` on existing theorems with `no_index` on the LHS.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR ensures
norm_castdoesn't fail to act in the presence ofno_indexannotationsWhile #2867 exists, it is necessary to put
no_indexaroundOfNat.ofNatin simp lemmas.This results in extra
Expr.mdatanodes, which must be removed before checking forofNatnumerals.