convenience offered by agda-mode: automatic generation of case analysis, refinement of holes, autocompletion of code based on types to name a few. http://lambda.jstolarek.com/2013/12/idris-first-impressionsi...