Search results

Make incomplete proofs more prominent

Status: Open.

#337 In leanprover/vscode-lean;

· DanielFabian opened on Aug 1, 2023

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

Status: Open.

#336 In leanprover/vscode-lean;

· kevinsullivan opened on Mar 20, 2023

Trouble setting up: lean.executablePath incorrect

Status: Open.

#335 In leanprover/vscode-lean;

· minimario opened on Mar 18, 2023

Waiting for Lean server to start...

Status: Open.

#333 In leanprover/vscode-lean;

· vithar1 opened on Feb 28, 2023

Feature request: Change default values for widget mode

Status: Open.

#327 In leanprover/vscode-lean;

· iulian-birlica opened on Jan 22, 2023

Feature request: highlight proof placeholders ("sorry")

Status: Open.

#320 In leanprover/vscode-lean;

· champignoom opened on Nov 23, 2022

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

Status: Open.

#297 In leanprover/vscode-lean;

· BoltonBailey opened on Apr 20, 2022

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

Status: Open.

#291 In leanprover/vscode-lean;

· lovettchris opened on Feb 17, 2022

command 'lean.displayGoal' not found

Status: Open.

#280 In leanprover/vscode-lean;

· FinalFantasy27 opened on Sep 6, 2021

Fast Install on MacOS Gives jroesch.lean DeprecationWarning and UnhandledPromiseRejectionWarning

Status: Open.

#279 In leanprover/vscode-lean;

· agryman opened on Aug 7, 2021

Extract abbreviation part of plugin into own package.

Status: Open.

#278 In leanprover/vscode-lean;

· Invisible-Rabbit-Hunter opened on Jul 30, 2021

Only open info view for Markdown files in Lean projects

Status: Open.

#277 In leanprover/vscode-lean;

· inkytonik opened on Jul 7, 2021