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.

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

refactor: Array.feraseIdx: avoid have in definition #4074

Merged
merged 1 commit into from
May 6, 2024

Conversation

nomeata
Copy link
Contributor

@nomeata nomeata commented May 6, 2024

otherwise it remains in the equational theorem and may cause the
“unused have linter” to trigger. By moving the proof into
decreasing_by, the equational theorems are unencumbered by termination
arguments.

see also leanprover-community/batteries#690 (comment)

otherwise it remains in the equational theorem and may cause the
“unused have linter” to trigger. By moving the proof into
`decreasing_by`, the equational theorems are unencumbered by termination
arguments.

see also leanprover-community/batteries#690 (comment)
@nomeata nomeata requested a review from semorrison as a code owner May 6, 2024 07:53
@nomeata nomeata changed the title refactors: Array.feraseIdx: avoid have in definition refactor: Array.feraseIdx: avoid have in definition May 6, 2024
@nomeata nomeata enabled auto-merge May 6, 2024 07:56
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc May 6, 2024 08:07 Inactive
@nomeata nomeata added this pull request to the merge queue May 6, 2024
@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 6, 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 e0c1afd12d4fc6b0e520774959aed06bf122aba9 --onto e362b50fa95d6823e59dd706803a93c25e888535. (2024-05-06 08:10:45)

Merged via the queue into master with commit 6d22793 May 6, 2024
12 of 13 checks passed
@digama0
Copy link
Collaborator

digama0 commented May 6, 2024

What are the chances that this is fixed in the equation compiler so that it doesn't generate terms that violate the unused have linter?

@nomeata
Copy link
Contributor Author

nomeata commented May 6, 2024

That's plausible; it would entail removing unused have there. Didn't check yet how hard it would be.

The induction principle generator should then also remove them from the minor premises.

Do you see a case where the user might genuinely want then to be there in the equations? In some cases it maybe might be nice to have them in the goal to intro them conveniently? But that sounds obscure, generating nicer equation lemmas is probably the better trade off.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

3 participants