Idris — це просто мрія ледачого програміста, із idris-vim код пишеться буквально сам собою.

Наприклад, хочемо ми відсортувати список певної довжини insertion sort’ом. Гаразд, пишемо

ins_sort : Ord el => Vect n el -> Vect n el

і говоримо Віму \d (define). Він зв’язується із repl Ідріса і дописує внизу:

ins_sort xs = ?ins_sort_rhs

де ?ins_sort_rhs це дірка, функціональність, уже правильно типізована, тільки ще не написана.

Ясно, що після цього нам хочеться розкласти xs на можливі клози pattern matching. Наводимо курсор на xs, говоримо \c (clauses), Вім переписує визначення в

ins_sort [] = ?ins_sort_rhs_1
ins_sort (x :: xs) = ?ins_sort_rhs_2

Заміняти ?ins_sort_rhs_1 на [] нижче нашої гідності (ми ж наче розумні люди, хай цим займаються інструменти), тому знову можна навести курсор на нього і сказати \o (prOOf search) — і ?ins_sort_rhs_1 сам перепишеться в []

Із ?ins_sort_rhs_2 інструмент уже почувається не таким розумним і доводиться писати код вручну:

ins_sort (x :: xs) = 
   let xs_sorted = ins_sort xs
   in ?sorted_insert

— зате тепер можна навести курсор на ?sorted_insert і зробити із нього нову проблему^W лемму^W функцію за допомогою \l (make Lemma). Вім вставляє нову функцію, якій передає як параметри всі локальні змінні:

sorted_insert : Ord el => 
                 (x : el) -> (xs : Vect k el) -> (xs_sorted : Vect k el)
                 -> Vect (S k) el

Ясно, що старі xs нам тепер не потрібні, доводиться підправляти цей код у

sorted_insert : Ord el => (x : el) -> (xs : Vect k el) -> Vect (S k) el

(де xs — це коротше ім’я для xs_sorted). Знову робимо \d, автоматично пишеться

sorted_insert x xs = ?sorted_insert_rhs

Наводимо курсор на xs, тиснемо \c, створюються клози:

sorted_insert x [] = ?sorted_insert_rhs_1
sorted_insert x (y :: xs) = ?sorted_insert_rhs_2

(зверніть увагу на автоматичне перейменування в y :: xs!).

За допомогою \o ?sorted_insert_rhs_1 автоматично переписується в [x]. Тепер можна зайнятись ?sorted_insert_rhs_2, тепер уже вручну:

sorted_insert x (y :: xs) = 
     if x < y then (x :: y :: xs) else y :: sorted_insert x xs

І вуаля, \r (reload) перевіряє типи в модулі, все нормально. Прямо з Віма пробуємо \e (expression/evaluate?), вводимо ins_sort [5,1,4,3,2] і в вікні Віма (яке з’являється по \i, interactive?) бачимо відповідь:

= [1, 2, 3, 4, 5] : Vect 5 Integer