Skip to content


Subversion checkout URL

You can clone with
Download ZIP
Vim/tmux 'mode' for Idris attempting to get something similar to what Agda and Coq/Proof General folk get on Emacs
VimL Perl
branch: master

Fetching latest commit…

Cannot retrieve the latest commit at this time

Failed to load latest commit information.

Emacs gets all the cool modes

So here's my attempt to make things a bit more smooth for vim.

Rather than using :e in Idris to load your EDITOR, idris-mode uses a script to start a tmux session with two panes: one on the left for editing Idris code using Vim and one on the right for running the Idris repl.

Using some vimscript it creates an Emacs-like mode so that you can see the code you're working on and the state of the Idris repl at the same time.


idris-mode requires:


Start idris-mode using by running:


script in your Idris project folder. You can put this script somewhere in your path, or symlink it, or whatever you prefer.

This will load a tmux session with a vim pane on the left and a idris session on the right.

Default leader keys

I have set up the plugin with some defaulted leader keys. If you'd rather I didn't let me know.

  • <leader>ih displays Idris help on the Idris pane.
  • <leader>il will take the current vim buffer and load it into Idris.
  • <leader>ir will reload the current file.
  • <leader>ic will compile the current file (giving it the same name minus file type).
  • <leader>im shows the remaining metavariables to be proven.
  • <leader>ip looks for a metavariable in the code and starts a proof of that hole.
  • <leader>ia Assumes :a done in Idris repl pane first. Moves the proof below where the proven metavariable occurs
  • <leader>iq quits Idris and closes the Idris pane.

If you are editing an idris file and save, an autocommand will load it into idris and thereby checking it for type correctness. This pretty much makes <leader>ir redundant... But you never know.

Known Problems

Some weird file loading stuff goes on when trying to send :a to the idris pane followed by trying to reload the file and move the proof. So right now after proving a metavariable in Idris repl, you have to:

  • :a in the Idris repl
  • move back to the vim pane
  • <leader>ia to reload the file and move the proof just below the metavariable

idris-mode has also only been tested on really simple files, like test2.idr. I can't guarantee that moving the proof will always be correct. So at the moment if it does get placed wrong, you'll need to tweak it manually.

Issues, Pull Requests, etc

If you find any problems, create an issue and supply the code and the commands you are trying so that I can reproduce and fix it. Either that or create a Pull Request :)

Something went wrong with that request. Please try again.