Sergey Sinchuk
Sergey Sinchuk
In the updated Intellij IDEA interface there is a new breadcrumbs bar and it is currently not suported by Arend plugin: Arend (internal structure within the file is not shown):...
Currently the items listed in the File Structure menu (Alt+7) are not navigable in Arend (unlike their Java/Kotlin counterparts).
Unmarking directory as a source root sometimes does not always propagate this change to YAML file. In this gif there's an example of a correct behavior for arend-lib and an...
``` 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...