idris-hackers/idris-mode — pull request #252 by david-christiansen (2014-09-24 12:22:03+00:00)
Title: Support :printdef over IDESlave

This adds the option to see the internal definition of a symbol to
right-click menus, as well as a command. There's no keybinding by
default.

Relies on https://github.com/idris-lang/Idris-dev/pull/1543.