Konstantin Nisht

You could make exceptions be more noticeable. Errors in other IDEA plugins are shown in red popup window, but these exceptions were discovered when I was inspecting my idea.log. Ok,...

Turns out no one suspected that it is possible. Ironically, I have this approach implemented in my other plugin (https://github.com/JetBrains/intellij-community/blob/master/plugins/groovy/groovy-psi/src/org/jetbrains/plugins/groovy/lang/parser/groovy.bnf), and it is fine there. But I thought that Arend...

I don't think that the \ entry should be painted in red color if it is a valid option.

Wow, the platform is so thoughtful about the plugins.

I have no idea where an NPE could occur on this line. Please report it again if you meet it.

Please consider implementing this feature via tracer, not via corresponded subexpr. Tracer provides much better results.

Regarding https://github.com/agda/agda/issues/1209: my termination checker does not permit these functions. For example, in https://github.com/agda/agda/issues/1209#issuecomment-129029486, the problematic function looks like ```agda inh : Stream D force inh = lim inh ,...

I am not aware of any problems connected with `--cubical`. The core principle here is that my checker tries to resemble System F which it is based on, and if...

@nad I fixed this problem I also enabled preprocessing by default, as was discussed during the Agda dev meeting. The slowdown on the standard library is negligible: on my machine,...

I agree, let's postpone the feature. I don't think it has acceptable quality for the release.