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

Hover should show full name of declaration #749

Closed
Kha opened this issue Oct 29, 2021 · 1 comment · Fixed by #811
Closed

Hover should show full name of declaration #749

Kha opened this issue Oct 29, 2021 · 1 comment · Fixed by #811
Labels
enhancement New feature or request good first issue Good for newcomers

Comments

@Kha
Copy link
Member

Kha commented Oct 29, 2021

When hovering over a declaration, including its namespaces in the hover would yield valuable information without taking up too much space. The type should probably be rendered as before, however, since it can potentially contain many names.
@Kha Kha added enhancement New feature or request good first issue Good for newcomers labels Oct 29, 2021
@gebner
Copy link
Member

gebner commented Oct 29, 2021

Yes!! And it would also be great if hover worked on the declaration name (for the same reason: to see the fully-qualified name):

def foo (x) : Nat := ...
   --^ Bar.foo : (x : String) → Nat

@larsk21 larsk21 mentioned this issue Nov 19, 2021
Merged
@Kha Kha closed this as completed in #811 Nov 21, 2021
ChrisHughes24 pushed a commit to ChrisHughes24/lean4 that referenced this issue Dec 2, 2022
@kim-em
port: several files from category_theory (leanprover#749)
c5ffca6 
mathlib git sha: 8350c34a64b9bc3fc64335df8006bffcadc7baa6

Also ports the reassoc attribute.

- [x] depends on: leanprover#755 

Co-authored-by: Scott Morrison <[email protected]>
ChrisHughes24 pushed a commit to ChrisHughes24/lean4 that referenced this issue Dec 2, 2022
@kim-em
feat: port Combinatorics.Quiver.Path (leanprover#811)
a764138 
Mathlib3 SHA : 62a5626868683c104774de8d85b9855234ac807c

- [ ] depends on: leanprover#749
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
enhancement New feature or request good first issue Good for newcomers
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Show fully-qualified name in hover text larsk21/lean4
2 participants
@Kha @gebner