idris-hackers/idris-mode — pull request #87 by david-christiansen (2014-02-19 08:49:45+00:00)
Title: Pervasive type and docs lookup

This relies on https://github.com/idris-lang/Idris-dev/pull/910 to work properly.

Now, C-c C-t works in every idris-mode buffer that makes sense, including the REPL, compiler errors, and type lookup info buffers. Additionally, a new command C-c C-d looks up documentation strings for symbols. Adding a clause is rebound to C-c C-s (for "start defining").