GitHub / edwinb/idris2-vim issues and pull requests
#32 - Link to `Interactive Idris editing with vim` goes to private wordpress page
Issue -
State: open - Opened by ShaunApps over 2 years ago
#31 - Installation on Vim 8.
Pull Request -
State: open - Opened by domandlj about 3 years ago
#30 - Add 'proof' keyword
Pull Request -
State: open - Opened by eayus almost 4 years ago
#29 - Explain that `<LocalLeader>` is `\` by default
Pull Request -
State: open - Opened by joliss over 4 years ago
#28 - Fix bug in IWrite causing Idris to not see changes.
Pull Request -
State: open - Opened by CodingCellist over 4 years ago
#27 - Help with Pathogen
Pull Request -
State: open - Opened by stepancheg over 4 years ago
#26 - Plugin does not load correctly on neovim / vim-plug
Issue -
State: open - Opened by space-shell over 4 years ago
- 2 comments
#25 - Documentation: Add skeleton for interface
Pull Request -
State: open - Opened by JonathanLorimer over 4 years ago
#24 - Refactor and add the TypeAt command
Pull Request -
State: open - Opened by GustavoMF31 over 4 years ago
#23 - I do not even get syntax highlighting
Issue -
State: closed - Opened by hbr over 4 years ago
- 3 comments
#22 - Make idris-response buffer better behaved in terms of buflist and jumplist
Pull Request -
State: open - Opened by maurges over 4 years ago
#21 - Fix a very minor typo in the syntax file
Pull Request -
State: open - Opened by isti115 over 4 years ago
#20 - Fix positional error mentioned in #19
Pull Request -
State: open - Opened by WizardOfMenlo almost 5 years ago
- 1 comment
#19 - File error in --no-color: File Not Found
Issue -
State: open - Opened by yoeluk almost 5 years ago
- 6 comments
#18 - Option to remove ANSI color codes from response window
Pull Request -
State: closed - Opened by neriglissar almost 5 years ago
- 1 comment
#17 - Add --no-color
Pull Request -
State: closed - Opened by Russoul about 5 years ago
- 1 comment
#16 - Disable color and minor syntax additions
Pull Request -
State: closed - Opened by ShinKage about 5 years ago
- 1 comment
#15 - Not working at all
Issue -
State: open - Opened by CTHULHU-Jesus about 5 years ago
- 1 comment
#14 - Syntastic does not work out of the box
Issue -
State: open - Opened by freddi301 about 5 years ago
#13 - Fix mapping for adding initial clause
Pull Request -
State: open - Opened by vmarkushin about 5 years ago
- 1 comment
#12 - MakeLemma doesn't transport erasable implicit arguments that must be explicitly bound for type checking
Issue -
State: closed - Opened by stephen-smith over 5 years ago
- 3 comments
#11 - Case splitting inserts invalid code that uses "$resolvedXXX" as an identifer.
Issue -
State: closed - Opened by stephen-smith over 5 years ago
- 1 comment
#10 - MakeWith is broken
Issue -
State: open - Opened by stephen-smith over 5 years ago
#9 - Fix a bug where 'file' is undefined.
Pull Request -
State: closed - Opened by jinwoo over 5 years ago
- 2 comments
#8 - Updated idris2 syntax highlighting
Pull Request -
State: closed - Opened by ShinKage over 5 years ago
- 1 comment
#7 - Further "Idris" -> "Idris 2" renamings were done
Pull Request -
State: closed - Opened by buzden over 5 years ago
- 1 comment
#6 - Variable `file` was replaced with an expression
Pull Request -
State: closed - Opened by buzden over 5 years ago
- 1 comment
#5 - [Fix] E121: Undefined variable: file in IdrisReload
Pull Request -
State: closed - Opened by neriglissar over 5 years ago
- 1 comment
#4 - Escape the paths passed to idris2
Pull Request -
State: closed - Opened by ShinKage over 5 years ago
- 2 comments
#3 - Resolve undefined reference error
Pull Request -
State: closed - Opened by mx00s over 5 years ago
- 2 comments
#2 - Use absolute paths to invoke Idris2
Pull Request -
State: closed - Opened by ziman over 5 years ago
- 1 comment
#1 - fix references to idris1(-mode) in README.md
Pull Request -
State: closed - Opened by mrkgnao over 5 years ago
- 1 comment