idris-hackers/idris-mode — pull request #116 by david-christiansen (2014-04-19 07:29:44+00:00)
Title: Support new :refine command

This relies on a merge of
https://github.com/idris-lang/Idris-dev/pull/1083

The keybinding C-c C-r is based on Agda's default binding for refine.