Issues

• Make incomplete proofs more prominent

  leanprover/vscode-lean#337 · Filter by author DanielFabian opened on Aug 1, 2023
  2

• Lines of tildes in comments screw up Lean parsing in this plugin

  leanprover/vscode-lean#336 · Filter by author kevinsullivan opened on Mar 20, 2023

• Trouble setting up: lean.executablePath incorrect

  leanprover/vscode-lean#335 · Filter by author minimario opened on Mar 18, 2023

• Waiting for Lean server to start...

  leanprover/vscode-lean#333 · Filter by author vithar1 opened on Feb 28, 2023
  2

• Feature request: Change default values for widget mode

  leanprover/vscode-lean#327 · Filter by author iulian-birlica opened on Jan 22, 2023

• Feature request: highlight proof placeholders ("sorry")

  leanprover/vscode-lean#320 · Filter by author champignoom opened on Nov 23, 2022

• Feature Request: Show type signature on mouseover of lemma names in definition

  leanprover/vscode-lean#297 · Filter by author BoltonBailey opened on Apr 20, 2022

• This lean 3 extension crashes the runTest when you close all document windows

  leanprover/vscode-lean#291 · Filter by author lovettchris opened on Feb 17, 2022

• command 'lean.displayGoal' not found

  leanprover/vscode-lean#280 · Filter by author FinalFantasy27 opened on Sep 6, 2021

• Fast Install on MacOS Gives jroesch.lean DeprecationWarning and UnhandledPromiseRejectionWarning

  leanprover/vscode-lean#279 · Filter by author agryman opened on Aug 7, 2021

• Extract abbreviation part of plugin into own package.

  leanprover/vscode-lean#278 · Filter by author Invisible-Rabbit-Hunter opened on Jul 30, 2021
  4

• Only open info view for Markdown files in Lean projects

  leanprover/vscode-lean#277 · Filter by author inkytonik opened on Jul 7, 2021

• Hover information for definitions using parameters is misleading

  leanprover/vscode-lean#275 · Filter by author eric-wieser opened on Jun 21, 2021
  2

• Mardown highlighting in comments consumes closing -/

  leanprover/vscode-lean#274 · Filter by author eric-wieser opened on Jun 2, 2021
  3

• "Try this" doesn't work correctly when there is an end in the line

  leanprover/vscode-lean#271 · Filter by author shingtaklam1324 opened on May 28, 2021

• Check for wrong lean version

  leanprover/vscode-lean#264 · Filter by author jldodds opened on May 6, 2021

• Eager replacement of abbreviations destroys redo history

  leanprover/vscode-lean#259 · Filter by author mhuisi opened on Feb 18, 2021
  2

• Abbreviations / Unicode-Input Improvement Discussion

  leanprover/vscode-lean#248 · Filter by author hediet opened on Jan 2, 2021
  2

• "Try this" does not work for unsaved buffers

  leanprover/vscode-lean#247 · Filter by author eric-wieser opened on Jan 1, 2021

• Live Preview Of Abbreviation Symbols

  leanprover/vscode-lean#245 · Filter by author hediet opened on Dec 30, 2020

• Intellisense For Abbreviations

  leanprover/vscode-lean#244 · Filter by author hediet opened on Dec 30, 2020

• Enable Strict Null Checks

  leanprover/vscode-lean#243 · Filter by author hediet opened on Dec 30, 2020

• Brackets in comments cause problems with "Try this"

  leanprover/vscode-lean#235 · Filter by author shingtaklam1324 opened on Nov 24, 2020
  1

• Change folding style

  leanprover/vscode-lean#232 · Filter by author Tasiro opened on Nov 9, 2020

• leanproject integration

  leanprover/vscode-lean#228 · Filter by author bryangingechen opened on Oct 22, 2020