3 ms·
Does Agda have any significant proof automation yet compared to say Coq? If not, how practical is it to use?
by seanwilson 12y ago
Does Agda have any significant proof automation yet compared to say Coq? If not, how practical is it to use?
- musername 12y agothere is an agda shell for interactice proving in emacs, with some automations. 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-impressionsions/ http://lambda.jstolarek.com/2013/12/idris-first-impressionsi...