• Stars
    star
    223
  • Rank 178,458 (Top 4 %)
  • Language
    Vim Script
  • Created about 11 years ago
  • Updated about 4 years ago

Reviews

There are no reviews yet. Be the first to send feedback to the community and the maintainers!

Repository Details

Idris mode for vim

Idris mode for vim

This is an Idris mode for vim which features syntax highlighting, indentation and optional syntax checking via Syntastic. If you need a REPL I recommend using Vimshell.

Screenshot

Installation

I recommend using Pathogen for installation. Simply clone this repo into your ~/.vim/bundle directory and you are ready to go.

cd ~/.vim/bundle
git clone https://github.com/idris-hackers/idris-vim.git

Manual Installation

Copy content into your ~/.vim directory.

Be sure that the following lines are in your .vimrc

syntax on
filetype on
filetype plugin indent on

Features

Apart from syntax highlighting, indentation, and unicode character concealing, idris-vim offers some neat interactive editing features. For more information on how to use it, read this blog article by Edwin Brady on Interactive Idris editing with vim.

Interactive Editing Commands

Idris mode for vim offers interactive editing capabilities, the following commands are supported.

<LocalLeader>r reload file

<LocalLeader>t show type

<LocalLeader>d Create an initial clause for a type declaration.

<LocalLeader>b Same as \d but for an initial typeclass method impl.

<LocalLeader>md Same as \d but for a proof clause

<LocalLeader>c case split

<LocalLeader>mc make case

<LocalLeader>w add with clause

<LocalLeader>e evaluate expression

<LocalLeader>l make lemma

<LocalLeader>m add missing clause

<LocalLeader>f refine item

<LocalLeader>o obvious proof search

<LocalLeader>p proof search

<LocalLeader>i open idris response window

<LocalLeader>h show documentation

Configuration

Indentation

To configure indentation in idris-vim you can use the following variables:

  • let g:idris_indent_if = 3

      if bool
      >>>then ...
      >>>else ...
    
  • let g:idris_indent_case = 5

      case xs of
      >>>>>[]      => ...
      >>>>>(y::ys) => ...
    
  • let g:idris_indent_let = 4

      let x = 0 in
      >>>>x
    
  • let g:idris_indent_where = 6

      where f : Int -> Int
      >>>>>>f x = x
    
  • let g:idris_indent_do = 3

      do x <- a
      >>>y <- b
    
  • let g:idris_indent_rewrite = 8

      rewrite prf in expr
      >>>>>>>>x
    

Concealing

Concealing with unicode characters is off by default, but let g:idris_conceal = 1 turns it on.

Tab Characters

If you simply must use tab characters, and would prefer that the ftplugin not set expandtab add let g:idris_allow_tabchar = 1.

More Repositories

1

software-foundations

Software Foundations in Idris
Idris
453
star
2

idris-mode

Idris syntax highlighting, compiler-supported editing, interactive REPL and more things for Emacs.
Emacs Lisp
256
star
3

idris-demos

Collection of Idris tests and demonstration programs
Idris
189
star
4

idris-koans

Koans are small lessons on the path to enlightenment. The aim of the Idris Koans project is to provide an easy learning environment in Idris. Your insight will be derived by encountering failing code and fixing them so that they type check.
Idris
172
star
5

idris-crypto

Implementation of cryptographic primitives using Idris
Idris
120
star
6

IdrisWeb

A secure web framework, built in the Idris language.
TeX
108
star
7

atom-language-idris

A Idris Mode for Atom.io
TypeScript
99
star
8

IdrisScript

FFI Bindings to interact with the unsafe world of JavaScript
Idris
88
star
9

idris-llvm

Idris LLVM codegen factored out
Haskell
77
star
10

idris-java

Java Code Generator for Idris
Haskell
71
star
11

iQuery

Idris Lib to interact with the DOM and Browser API for the JavaScript backend
Idris
40
star
12

idris-posix

System POSIX bindings for Idris.
Idris
34
star
13

idrispkgs

Old Nix expressions for Idris packaging. Idris support moved into Nixpkgs!
Nix
28
star
14

idris-sublime

A Plugin to use Idris with Sublime
Python
27
star
15

idris-free

Free Monads and useful constructions to work with them
Idris
25
star
16

eff-tutorial

An old tutorial for using `Effects` in Idris.
TeX
24
star
17

idris-cph-exercises

Exercises from the Idris lecture series presented at the ITU Copenhagen on March 11--15, updated to work with latest Idris releases.
Idris
23
star
18

idris-lens

Idris
22
star
19

idris-algebra

This is an attempt at painting as many bikesheds as possible with a typeclass hierarchy for idris reflecting "Algebra"
Idris
18
star
20

usb

libusb binding for idris and Effectful USB programming
C
11
star
21

idris-bot

An IRC bot connected to an Idris REPL
Haskell
10
star
22

idris-java-rts

Java Runtime System for the Idris Programming Language
Java
10
star
23

idris-extras

Various minor modes for editors and some tool support.
TeX
6
star
24

idris-array

primitive flat arrays containing Idris values
Idris
6
star
25

idris-time

A dependently-typed implementation of ISO 8601.
3
star