edwinb idris2-vim issues

edwinb / idris2-vim

Vim mode for Idris 2

75 stars 26 forks source link

issues

Newest

Newest Most commented Recently updated Oldest Least commented Least recently updated

Link to `Interactive Idris editing with vim` goes to private wordpress page

#32 ShaunApps opened 1 year ago
0
Installation on Vim 8.

#31 domandlj opened 2 years ago
0
Add 'proof' keyword

#30 eayus opened 3 years ago
0
Explain that `<LocalLeader>` is `\` by default

#29 joliss opened 3 years ago
0
Fix bug in IWrite causing Idris to not see changes.

#28 CodingCellist opened 3 years ago
0
Help with Pathogen

#27 stepancheg opened 3 years ago
0
Plugin does not load correctly on neovim / vim-plug

#26 space-shell opened 3 years ago
2
Documentation: Add skeleton for interface

#25 JonathanLorimer opened 3 years ago
0
Refactor and add the TypeAt command

#24 GustavoMF31 opened 3 years ago
0
I do not even get syntax highlighting

#23 hbr closed 3 years ago
3
Make idris-response buffer better behaved in terms of buflist and jumplist

#22 maurges opened 3 years ago
0
Fix a very minor typo in the syntax file

#21 isti115 opened 3 years ago
0
Fix positional error mentioned in #19

#20 WizardOfMenlo opened 3 years ago
1
File error in --no-color: File Not Found

#19 yoeluk opened 3 years ago
6
Option to remove ANSI color codes from response window

#18 neriglissar closed 4 years ago
1
Add --no-color

#17 Russoul closed 4 years ago
1
Disable color and minor syntax additions

#16 ShinKage closed 3 years ago
1
Not working at all

#15 CTHULHU-Jesus opened 4 years ago
1
Syntastic does not work out of the box

#14 freddi301 opened 4 years ago
0
Fix mapping for adding initial clause

#13 vmarkushin opened 4 years ago
1
MakeLemma doesn't transport erasable implicit arguments that must be explicitly bound for type checking

#12 stephen-smith closed 4 years ago
3
Case splitting inserts invalid code that uses "$resolvedXXX" as an identifer.

#11 stephen-smith closed 4 years ago
1
MakeWith is broken

#10 stephen-smith opened 4 years ago
0
Fix a bug where 'file' is undefined.

#9 jinwoo closed 4 years ago
2
Updated idris2 syntax highlighting

#8 ShinKage closed 4 years ago
1
Further "Idris" -> "Idris 2" renamings were done

#7 buzden closed 4 years ago
1
Variable `file` was replaced with an expression

#6 buzden closed 4 years ago
1
[Fix] E121: Undefined variable: file in IdrisReload

#5 neriglissar closed 4 years ago
1
Escape the paths passed to idris2

#4 ShinKage closed 4 years ago
2
Resolve undefined reference error

#3 mx00s closed 4 years ago
2
Use absolute paths to invoke Idris2

#2 ziman closed 4 years ago
1
fix references to idris1(-mode) in README.md

#1 mrkgnao closed 4 years ago
1