[thrw1q]

Those videos on the Idris mode are also very impressive:

https://www.youtube.com/channel/UCsON_8vogp4nCQFTnfu43kA

(Other languages also have nice modes for context-aware completion (and more), like Haskell's ghc-mod and Rust's racer, which is incomplete but is already very nice)

[pmoriarty]

Or take a look at the videos at Emacs Rocks.[1]

[1] - http://emacsrocks.com/