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

rintro error message is in the wrong place #5659

Closed
3 tasks done
TwoFX opened this issue Oct 9, 2024 · 1 comment · Fixed by #6565
Closed
3 tasks done

rintro error message is in the wrong place #5659

TwoFX opened this issue Oct 9, 2024 · 1 comment · Fixed by #6565
Labels
bug Something isn't working P-medium We may work on this issue if we find the time

Comments

@TwoFX
Copy link
Member

TwoFX commented Oct 9, 2024

Prerequisites

Please put an X between the brackets as you perform the following steps:

Description

In the code

example : (∃ n : Nat, n < 0) → False := by
  rintro ⟨n, hn⟩ h

the red squigglies for the tactic 'introN' failed, insufficient number of binders error message are under the hn, which makes no sense. When using intro instead of rintro, the entire line is highlighted.

Steps to Reproduce

  1. Copy the above code into live.lean-lang.org

Expected behavior: Either only h or the entire line should be highlighted

Actual behavior: Only hn is highlighted.

Versions

4.12.0-nightly-2024-10-08 on live.lean-lang.org

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.
@TwoFX TwoFX added the bug Something isn't working label Oct 9, 2024
@digama0
Copy link
Collaborator

digama0 commented Oct 9, 2024

The error should be on the h.

@leanprover-bot leanprover-bot added the P-medium We may work on this issue if we find the time label Oct 18, 2024
sgraf812 added a commit that referenced this issue Jan 7, 2025
@sgraf812
fix: proper "excess binders" error locations for rintro and intro (…
05602a7 
…#5659)

Add a few `withRef` wrappers to invokations of `MVarId.intro` to fix
error locations. Perhaps `MVarId.intro` should take a syntax object
to set the location itself in the future; however there are a couple
other call sites which would need non-trivial fixup.

Closes #5659.
@sgraf812 sgraf812 mentioned this issue Jan 7, 2025
Merged
sgraf812 added a commit that referenced this issue Jan 7, 2025
@sgraf812
fix: proper "excess binders" error locations for rintro and intro (…
c5e1efc 
…#5659)

Add a few `withRef` wrappers to invokations of `MVarId.intro` to fix
error locations. Perhaps `MVarId.intro` should take a syntax object
to set the location itself in the future; however there are a couple
other call sites which would need non-trivial fixup.

Closes #5659.
sgraf812 added a commit that referenced this issue Jan 8, 2025
@sgraf812
fix: proper "excess binders" error locations for rintro and intro (…
2635c86 
…#5659)

Add a few `withRef` wrappers to invokations of `MVarId.intro` to fix
error locations. Perhaps `MVarId.intro` should take a syntax object
to set the location itself in the future; however there are a couple
other call sites which would need non-trivial fixup.

Closes #5659.
github-merge-queue bot pushed a commit that referenced this issue Jan 8, 2025
@sgraf812
fix: proper "excess binders" error locations for rintro and intro (…
f01471f 
…#6565)

This PR fixes the location of the error emitted when the `rintro` and
`intro` tactics cannot introduce the requested number of binders.

This patch adds a few `withRef` wrappers to invocations of
`MVarId.intro` to fix error locations. Perhaps `MVarId.intro` should
take a syntax object to set the location itself in the future; however
there are a couple other call sites which would need non-trivial fixup.

Closes  #5659.
luisacicolini pushed a commit to opencompl/lean4 that referenced this issue Jan 21, 2025
@sgraf812 @luisacicolini
fix: proper "excess binders" error locations for rintro and intro (…
0fa8282 
…leanprover#6565)

This PR fixes the location of the error emitted when the `rintro` and
`intro` tactics cannot introduce the requested number of binders.

This patch adds a few `withRef` wrappers to invocations of
`MVarId.intro` to fix error locations. Perhaps `MVarId.intro` should
take a syntax object to set the location itself in the future; however
there are a couple other call sites which would need non-trivial fixup.

Closes  leanprover#5659.
JovanGerb pushed a commit to JovanGerb/lean4 that referenced this issue Jan 21, 2025
@sgraf812 @JovanGerb
fix: proper "excess binders" error locations for rintro and intro (…
6067b5c 
…leanprover#6565)

This PR fixes the location of the error emitted when the `rintro` and
`intro` tactics cannot introduce the requested number of binders.

This patch adds a few `withRef` wrappers to invocations of
`MVarId.intro` to fix error locations. Perhaps `MVarId.intro` should
take a syntax object to set the location itself in the future; however
there are a couple other call sites which would need non-trivial fixup.

Closes  leanprover#5659.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
bug Something isn't working P-medium We may work on this issue if we find the time
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

fix: proper "excess binders" error locations for rintro and intro leanprover/lean4
3 participants
@digama0 @TwoFX @leanprover-bot