Skip to content

Issues: zjhmale/vscode-idris

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.

Sign up for GitHub

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

20 Open 91 Closed
20 Open 91 Closed
Author
Filter by author
Label
Filter by label
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Milestones
Filter by milestone
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

Support idris2
#132 opened Oct 4, 2020 by turion
4
suggestions appear before quickSuggestionDelay
#129 opened Mar 12, 2020 by sourcefrog
Cannot run extension on Windows
#128 opened Feb 26, 2020 by Pzixel
7
Output channel is focused
#124 opened Oct 8, 2018 by jasper-d
1
2
make-lemma seem don't work
#123 opened Jun 7, 2018 by jiamo
line number and column snippet is not shown when evaluating idris code
#121 opened Apr 28, 2018 by bbarker
Default Keyboard Shortcuts
#120 opened Mar 4, 2018 by namuol
3
I think my settings are wrong. - 'idris.typecheck'
#119 opened Dec 5, 2017 by DUVELA
2
idris.typecheck command stops working
#118 opened Aug 6, 2017 by ruippeixotog
8
New lines are incorrect for some multi-line hints
#117 opened Jul 26, 2017 by varosi
"Generate initial pattern match clause" doesn't respect LIDR syntax
#116 opened Jul 14, 2017 by clayrat
"Generate initial pattern match clause" doesn't respect multiline signatures
#115 opened Jul 14, 2017 by clayrat
v0.9.8 broken on Windows bug windows related
#113 opened Jun 9, 2017 by dcastro
@zjhmale
18
Icon & Website working in progress
#78 opened Apr 15, 2017 by zjhmale
2 tasks
@zjhmale
Support formatter discussion
#77 opened Apr 14, 2017 by zjhmale
More sophisticated test cases
#47 opened Mar 29, 2017 by zjhmale
Completion improvement
#31 opened Mar 26, 2017 by zjhmale
1 of 2 tasks
@zjhmale
10
Support more commands
#30 opened Mar 26, 2017 by zjhmale
3 of 10 tasks
@zjhmale
7
Better representations of errors enhancement pending
#23 opened Mar 19, 2017 by zjhmale
1 of 3 tasks
@be5invis @zjhmale
2
Language Server Protocol working in progress
#8 opened Jan 4, 2017 by zjhmale
@zjhmale
ProTip! Mix and match filters to narrow down what you’re looking for.