This repository has been archived by the owner on Jun 26, 2024. It is now read-only.
-
Notifications
You must be signed in to change notification settings - Fork 48
Issues: leanprover/vscode-lean
Author
Label
Projects
Milestones
Assignee
Sort
Issues list
Lines of tildes in comments screw up Lean parsing in this plugin
#336
opened Mar 20, 2023 by
kevinsullivan
Feature Request: Show type signature on mouseover of lemma names in definition
#297
opened Apr 20, 2022 by
BoltonBailey
This lean 3 extension crashes the runTest when you close all document windows
#291
opened Feb 17, 2022 by
lovettchris
Fast Install on MacOS Gives jroesch.lean DeprecationWarning and UnhandledPromiseRejectionWarning
#279
opened Aug 7, 2021 by
agryman
Extract abbreviation part of plugin into own package.
#278
opened Jul 30, 2021 by
Invisible-Rabbit-Hunter
Hover information for definitions using parameters is misleading
#275
opened Jun 21, 2021 by
eric-wieser
"Try this" doesn't work correctly when there is an
end
in the line
#271
opened May 28, 2021 by
shingtaklam1324
Previous Next
ProTip!
no:milestone will show everything without a milestone.