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.

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

fix: make rw [foo] look in the local context for foo before it looks in the environment #2738

Merged
merged 2 commits into from
Oct 30, 2023
Merged

fix: make rw [foo] look in the local context for foo before it looks in the environment #2738

merged 2 commits into from
Oct 30, 2023

Conversation

thorimur
Copy link
Contributor

@thorimur thorimur commented Oct 23, 2023 •
edited
Loading

Fixes #2729.

This requires some changes to mathlib4 where the opposite behavior was being exploited; we now must namespace foo to make it refer to a constant in the environment (e.g. rw [Bar.foo]), which has the nice side effect of making explicit which foo we're referring to. See leanprover-community/mathlib4#7872.

@github-actions
Copy link
Contributor

Thanks for your contribution! Please make sure to follow our Commit Convention.

@thorimur
Copy link
Contributor Author

WIP

@github-actions github-actions bot added the WIP This is work in progress, and only a PR for the sake of CI or sharing. No review yet. label Oct 23, 2023
@thorimur thorimur mentioned this pull request Oct 23, 2023
Closed
1 task
@thorimur thorimur force-pushed the rw-fvar-instead-of-const branch 2 times, most recently from 9563e5f to 2db94fe Compare October 23, 2023 07:11
@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 Oct 23, 2023
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 23, 2023
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#2738
b086345
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Oct 23, 2023
@leanprover-community-mathlib4-bot
Copy link
Collaborator

leanprover-community-mathlib4-bot commented Oct 23, 2023 •
edited
Loading

@thorimur thorimur mentioned this pull request Oct 23, 2023
Closed
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-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 Oct 23, 2023
@thorimur
Copy link
Contributor Author

awaiting-review

@github-actions github-actions bot added awaiting-review Waiting for someone to review the PR and removed WIP This is work in progress, and only a PR for the sake of CI or sharing. No review yet. labels Oct 23, 2023
@thorimur thorimur marked this pull request as ready for review October 24, 2023 02:54
semorrison
semorrison reviewed Oct 24, 2023
View reviewed changes
tests/lean/rwPrioritizesLCtxOverEnv.lean

example (A B : Prop) (foo : A ↔ B) (b : B) : A := by
rw [foo] -- should be interpreted as `foo : A ↔ B`, not `foo : List Nat`, and succeed
assumption
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think we need a test that shows that we can still rewrite by the global constant, by fully specifying it (e.g. with _root_).

Copy link
Contributor Author

@thorimur thorimur Oct 24, 2023 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Good point; added in c0e3492 (rebased for nicer commit history). :)

EDIT: now d84f159 (rebase to master)

@semorrison semorrison added the missing tests This PR requires the addition of tests before it can be merged. label Oct 24, 2023
@semorrison semorrison self-assigned this Oct 24, 2023
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 24, 2023
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#2738
77ce2f1
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan and removed builds-mathlib CI has verified that Mathlib builds against this PR labels Oct 24, 2023
@semorrison semorrison removed missing tests This PR requires the addition of tests before it can be merged. breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Oct 25, 2023
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 25, 2023
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#2738
fae6c5b
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Oct 26, 2023
@semorrison semorrison merged commit 50f2154 into leanprover:master Oct 30, 2023
16 checks passed
Komyyy pushed a commit to Komyyy/lean4 that referenced this pull request Nov 2, 2023
@thorimur @Komyyy
fix: make rw [foo] look in the local context for foo before it lo…
5f449c1 
…oks in the environment (leanprover#2738)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@semorrison semorrison semorrison left review comments

Assignees

@semorrison semorrison

Labels
awaiting-review Waiting for someone to review the PR breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan 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.

rw [h] uses h from the environment in preference to h from the local context
3 participants
@thorimur @leanprover-community-mathlib4-bot @semorrison