-
Notifications
You must be signed in to change notification settings - Fork 1
Issues: DenisGorbachev/vscode-lean4-code-actions
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
Author
Label
Projects
Milestones
Assignee
Sort
Issues list
bug: renaming file action iterates over dependencies
bug
Something isn't working
#21
opened Apr 29, 2024 by
joneugster
Wrap together Something new should be implemented
rw
or simp
tactics.
feature
#15
opened Aug 25, 2023 by
faenuccio
Reuse existing Something new should be implemented
variable
commands
feature
#14
opened Aug 25, 2023 by
DenisGorbachev
Shorten the code by adding Something new should be implemented
open ... in ...
commands
feature
#13
opened Aug 25, 2023 by
DenisGorbachev
Fold/unfold notations
feature
Something new should be implemented
#12
opened Aug 25, 2023 by
DenisGorbachev
Shorten the code by removing open namespaces from declarations
feature
Something new should be implemented
#11
opened Aug 25, 2023 by
DenisGorbachev
Implement a server-side "Move definition" command
feature
Something new should be implemented
#10
opened Aug 15, 2023 by
DenisGorbachev
Auto-import should also add or update the nearest Something new should be implemented
open
command
feature
#9
opened Aug 15, 2023 by
DenisGorbachev
Implement "rename primary definition"
feature
Something new should be implemented
#7
opened Aug 12, 2023 by
DenisGorbachev
Implement "toggle brackets"
feature
Something new should be implemented
#6
opened Aug 12, 2023 by
DenisGorbachev
Apply extension guidelines
documentation
Improvements or additions to documentation
#5
opened Aug 12, 2023 by
DenisGorbachev
ProTip!
no:milestone will show everything without a milestone.