Does Agda have any significant proof automation yet compared to say Coq? If not, how practical is it to use?
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...