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

Go to definition on import doesn't work on last module name #4958

Closed
Kha opened this issue Aug 8, 2024 · 0 comments · Fixed by #5170
Closed

Go to definition on import doesn't work on last module name #4958

Kha opened this issue Aug 8, 2024 · 0 comments · Fixed by #5170
Labels
bug Something isn't working P-high We will work on this issue

Comments

@Kha
Copy link
Member

Kha commented Aug 8, 2024 

import Init
--^ works ^ works
import Init
--^ works ^ doesn't
@Kha Kha added the bug Something isn't working label Aug 8, 2024
@leanprover-bot leanprover-bot added the P-high We will work on this issue label Aug 9, 2024
@Kha Kha mentioned this issue Aug 26, 2024
Merged
github-merge-queue bot pushed a commit that referenced this issue Aug 26, 2024
@Kha
fix: Syntax.unsetTrailing (#5170)
dcdbb9b 
Fixes #4958
@Kha Kha closed this as completed in #5170 Aug 26, 2024
github-actions bot pushed a commit that referenced this issue Aug 26, 2024
@Kha @github-actions
fix: Syntax.unsetTrailing (#5170)
a62fc0e 
Fixes #4958

(cherry picked from commit dcdbb9b)
tobiasgrosser pushed a commit to opencompl/lean4 that referenced this issue Aug 26, 2024
@Kha @tobiasgrosser
fix: Syntax.unsetTrailing (leanprover#5170)
167a9d5 
Fixes leanprover#4958
Kha added a commit that referenced this issue Aug 26, 2024
@Kha
fix: Syntax.unsetTrailing (#5170)
d017635 
Fixes #4958

(cherry picked from commit dcdbb9b)
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-high We will work on this issue
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

fix: Syntax.unsetTrailing Kha/lean4
2 participants
@Kha @leanprover-bot