用了一段时间Agda的感想

CoqIde agda-mode in Atom agda-mode in Emacs 相比之下，CoqIde编写代码的体验较好。三个分栏窗体提供的信息充足且格式完整。 不过agda-mode的编写体验也是挺好的，尤其是关于Hole的处理，个人感觉在一定程度上替代了Tactics的作用。而且通过类似latex方式，Unicode字符的输入也不是特别复杂。