Install

Install Idris with stack install idris on Ubuntu. Or download Windows binaries idris-1.3.1-win64.exe and run it, which is actually an executable zip file.

HelloWorld

cat << EOF > hello.idr
module Main
main : IO ()
main = putStrLn "Hello world"
EOF

idris hello.idr -o hello
./hello

Verified on Ubuntu 16.04 with Idris 1.3.1, 2019/3/11.

Workflow

In REPL run the script with :exec command:

$ idris hello.idr
*hello> :exec
Hello world

You can also use :? to list all command in REPL. For example :l (load script), :r (reload current file), :e (edit current file), :w (watch file changes), :doc (show doc of a function), :q (quit), etc.

Define local variable with :let, like :let aa = 3.

Run shell command with :!, like :! pwd.

Workflow in Editor

neovim

First install idris-vim with vim-plug: add Plug 'idris-hackers/idris-vim' into $MYVIMRC.

You must have a running Idris REPL to use this plugin. To fulfill this, you have 2 options:

• neovim terminal: open with :sp|term idris WordLength.idr, or :vsp|term for REPL in a vertical split window, or :tabe|term idris WordLength.idr for REPL in a new tab;

• An independent Idris REPL: run idris WordLength.idr in another console window;

To avoid keyboard shortcuts conflict, modify <LocalLeader>c :call IdrisCaseSplit()<ENTER> to <LocalLeader>ic :call IdrisCaseSplit()<ENTER> in the file $HOME/.config/nvim/plugged/idris-vim/ftplugin/idris.vim, where the added prefix i in shortcut represents Idris.

Then add prefix i for the shortcuts of IdrisReload, IdrisEval and other relevant functions in the same way;

The work-flow:

1. Open file WordLength.idr with nvim, write allLengths : List String -> List Nat;

2. Create an Idris REPL:

3. Put the cursor on allLengths and press <leader>id: the second line allLengths xs = ?allLengths_rhs will be created by the plugin. Under the hood, the function IdrisAddClause do the magic;

4. Put the cursor on xs and press <leader>ic in neovim (or C-M-c in VS Code), the second line becomes: allLengths [] = ?allLengths_rhs_1 allLengths (x :: xs) = ?allLengths_rhs_2 which are transformed by IdrisCaseSplit under the hood;

5. Put the cursor on ?allLengths_rhs_1 and press <leader>o, this expression becomes to [], which is implemented by IdrisProofSearch.

Other useful shortcuts:

• ,h: show doc;

• ,t: show type;

• ,ii: open response window;

• ,ir: reload file;

• ,ie: evaluate a expression;

• ,l (C-M-l): IdrisMakeLemma. Create a top-level function definition from a hole (put the curor on the target hole and use this shortcut). Then rename the generated function to what you want. See demo in TDDI, p72, step 5.

Note: :h idris-vim.txt for details of the Idris plugin.

VS Code

Install the Idris extension, and add the following lines into settings.json (open it with Ctrl-Shift-P, then open settings):

{
  ...
  "idris.executablePath": "d:/apps/idris-1.3.1/idris.exe",
  "idris.hoverMode": "fallback",
  "idris.suggestMode": "allWords",
  "idris.warnPartial": false,
  "idris.showOutputWhenTypechecking": false,
  "idris.numbersOfContinuousTypechecking": 10
}

Add the following lines into keybindings.json (open it with Ctrl-Shift-P, then open keyboard shortcuts:

{
  ...
  { "key": "alt+ctrl+a", "command": "idris.add-clause" },
  { "key": "alt+ctrl+t", "command": "idris.type-of" },
  { "key": "alt+ctrl+c", "command": "idris.case-split" },
  { "key": "alt+ctrl+r", "command": "idris.start-refresh-repl" }
}

Above shortcuts are following the definitions in section 3.1.1 in TDDI.