intellij-arend
intellij-arend copied to clipboard
JetBrains
Arend plugin for IntelliJ IDEA
``` java.lang.Throwable: Template presentations must not be used directly at com.intellij.openapi.actionSystem.Presentation.assertNotTemplatePresentation(Presentation.java:581) at com.intellij.openapi.actionSystem.Presentation.setEnabled(Presentation.java:545) at org.arend.toolWindow.errors.tree.ArendErrorTreeAutoScrollFromSource.createActionGroup(ArendErrorTreeAutoScrollFromSource.kt:130) at org.arend.toolWindow.errors.ArendMessagesView.(ArendMessagesView.kt:103) at org.arend.toolWindow.errors.ArendMessagesService.initView(ArendMessagesService.kt:53) at org.arend.toolWindow.errors.ArendMessagesFactory.createToolWindowContent(ArendMessagesFactory.kt:11) at com.intellij.openapi.wm.impl.ToolWindowImpl.createContentIfNeeded(ToolWindowImpl.kt:667) at com.intellij.openapi.wm.impl.ToolWindowImpl.scheduleContentInitializationIfNeeded$intellij_platform_ide_impl(ToolWindowImpl.kt:646) at com.intellij.openapi.wm.impl.ToolWindowManagerImpl.doShowWindow(ToolWindowManagerImpl.kt:1036) at com.intellij.openapi.wm.impl.ToolWindowManagerImpl.showToolWindowImpl(ToolWindowManagerImpl.kt:970) at...
Replace the usage of `simplify` tactic in `Module.*c_zro-left` with `{?}`. Then call "Generate function from goal" intention on the goal. ``` java.lang.IllegalStateException: Minimization of expression (E) is likely diverged. Please...
Simple recursive calls of a definition/theorem should be marked with a "recursive call" icon:  More complicated recursive calls (case of mutual recursion) should be marked with a special "mutual...
Implement charmap tool which will include symbol ranges which are supported by Arend lexer: 2200–22FF and 2A00–2AFF (probably categorized in some way). Alternatively, open the OS-provided charmap which would offer...
Currently Arend Messages panel shows: a) all error messages within all library files b) error messages are grouped with respect to the definition that contains them. It would be helpful...
In this example leading "-"'s are part of doc. comment syntax.  The example can be found in arend-lib/master
Current behavior of Implement missing fields/coclauses quickfix is unsatisfactory because it ignores the mechanism of default fields, see pic. In this example all the fields of `DecSet` except `decideEq` and...
Suppose that you are defining a function with an implicit parameter which also happens to be a class. ``` \instance DecWordMonoid (S : DecSet) : DecSet | E => List...
If one writes latex code that contains "{-" substring, the code analyser thinks that it opens another comment parenthesis. In reality it can be a part of latex code symbolising...
Here are 3 exceptions I got from routine working with plugin (I used Arend Messages View to view goals and error messages). The noticeable problem was that baloons which appear...