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)