issues
search
leanprover
/
vscode-lean
Extension for VS Code that provides support for the older Lean 3 language. Succeeded by vscode-lean4 ('lean4' in the extensions menu) for the Lean 4 language.
Apache License 2.0
116
stars
49
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
Documentation recourses broken
#343
fpvandoorn
closed
1 month ago
0
Fix link to widgets in mathlib3 documentation
#342
m4lvin
opened
2 months ago
0
Update display name to reflect version and deprecation
#341
mhuisi
closed
2 months ago
0
Update README to reflect that extension is for Lean 3
#339
mhuisi
closed
1 year ago
1
update README to clearly label as for Lean 3
#338
kim-em
closed
1 year ago
1
Make incomplete proofs more prominent
#337
DanielFabian
opened
1 year ago
2
Lines of tildes in comments screw up Lean parsing in this plugin
#336
kevinsullivan
opened
1 year ago
0
Trouble setting up: lean.executablePath incorrect
#335
minimario
opened
1 year ago
0
Add the two-sided abbreviation for <<>>
#334
Julian
closed
7 months ago
0
Waiting for Lean server to start...
#333
vithar1
opened
1 year ago
2
Bump terser from 5.7.0 to 5.16.3
#332
dependabot[bot]
opened
1 year ago
0
Bump minimist from 1.2.5 to 1.2.8
#331
dependabot[bot]
opened
1 year ago
0
Bump nth-check from 2.0.0 to 2.1.1
#330
dependabot[bot]
opened
1 year ago
0
Bump follow-redirects from 1.14.1 to 1.15.2
#329
dependabot[bot]
opened
1 year ago
0
Correct the symbol for perpendicular
#328
eric-wieser
closed
1 year ago
4
Feature request: Change default values for widget mode
#327
iulian-birlica
opened
1 year ago
0
Bump minimatch from 3.0.4 to 3.1.2
#326
dependabot[bot]
opened
1 year ago
0
Bump json5 from 2.1.3 to 2.2.3
#325
dependabot[bot]
opened
1 year ago
0
Bump express from 4.17.1 to 4.17.3
#324
dependabot[bot]
opened
1 year ago
0
Bump qs and express
#323
dependabot[bot]
opened
1 year ago
0
Correct the abbreviation for angle
#322
eric-wieser
closed
1 year ago
0
New API suggestion icon
#321
timlacroix
closed
1 year ago
1
Feature request: highlight proof placeholders ("sorry")
#320
champignoom
opened
1 year ago
0
fix(abbreviations.json): update norm symbol
#319
fpvandoorn
closed
1 year ago
3
Bump loader-utils from 2.0.0 to 2.0.4
#318
dependabot[bot]
opened
1 year ago
0
Bump loader-utils from 2.0.0 to 2.0.3
#317
dependabot[bot]
closed
1 year ago
1
Bump underscore and ovsx
#316
dependabot[bot]
opened
2 years ago
0
add abbreviations for `‖ ‖` which place the cursor inside
#315
j-loreaux
closed
1 year ago
3
Add suggest API defaults. Add Suggest button / API to README
#314
timlacroix
closed
2 years ago
0
Bump markdown-it, ovsx and vsce
#313
dependabot[bot]
opened
2 years ago
0
Proposal for an API based "Suggestions" detail in infoview
#312
timlacroix
closed
2 years ago
3
Do not do manual html escaping of react components
#311
eric-wieser
closed
2 years ago
8
Bump terser from 5.7.0 to 5.14.2
#310
dependabot[bot]
closed
1 year ago
1
Tweak the README now that bracket pair coloring is upstream.
#309
Julian
closed
2 years ago
0
"Try this:" fails on messages with quotation marks
#308
robertylewis
closed
2 years ago
1
feat(.gitpod): Add gitpod configuration
#307
eric-wieser
closed
2 years ago
0
feat(completion,search): show icons next to symbols
#306
eric-wieser
closed
2 years ago
0
Add support for listing symbols
#305
eric-wieser
closed
2 years ago
3
Fix 'try this' in untitled windows
#303
eric-wieser
closed
2 years ago
0
Add game shortcuts
#302
vihdzp
closed
2 years ago
0
fix: translate between utf16 code unit offsets (vscode) and codepoints (lean)
#301
eric-wieser
closed
2 years ago
1
Consider using `message.end_pos` in diagnostics
#300
eric-wieser
closed
2 years ago
2
Bump nanoid from 3.1.23 to 3.3.4
#299
dependabot[bot]
opened
2 years ago
0
Add weakly covers symbol and opposites shortcuts
#298
YaelDillies
closed
2 years ago
2
Feature Request: Show type signature on mouseover of lemma names in definition
#297
BoltonBailey
opened
2 years ago
0
Bump minimist from 1.2.5 to 1.2.6
#296
dependabot[bot]
closed
1 year ago
1
Bump nanoid from 3.1.23 to 3.3.1
#295
dependabot[bot]
closed
2 years ago
1
Bump ansi-regex from 5.0.0 to 5.0.1
#294
dependabot[bot]
opened
2 years ago
0
Bump nth-check from 2.0.0 to 2.0.1
#293
dependabot[bot]
closed
1 year ago
1
fix: some shutdown bugs found in CI testing with the lean3 extension.
#292
lovettchris
closed
2 years ago
0
Next