Sergey Sinchuk

The following issue has appeared after the recent upgrade on a new IDEA platform Commit: ba021f73206e14941e6437eb715ec5ad951bf0f6 Steps to reproduce: - Clone `arend-lang/tutorial-code` - Import `PartI` of the tutorial using import...

Implement `Ctrl+Shift+P` for patterns

1

This feature should support the following cases: Patterns in elimination blocks, case expressions, let expressions and lambda expressions.

Current implementation only allows you to see type information that has been dumped and stored during the typechecking process. Due to peculiarities of typechecking this process currently is not 100%...

- [ ] Group search results using refactoring-specific categories, specifically mention usages for which refactoring is not going to work, highlight tail-implicit usages. - [x] Keep track of typechecking errors,...

``` \data Empty \func foo : \Sigma (Empty -> Nat) Nat => (\lam e => (\case e), 0) ```

``` java.lang.Throwable: Write-unsafe context! Model changes are allowed from write-safe contexts only. Please ensure you're using invokeLater/invokeAndWait with a correct modality state (not "any"). See TransactionGuard documentation for details. current...

In this code sample `true` and `false` should be highlighted as variables, whose names clash with the names of the (unimported) constructors of the datatype Bool. ``` \import Data.Bool(Bool, if)...

Currently one can not use numerals when formulating a search query in proof searcher.

Reproducer: https://github.com/JetBrains/arend-lib/commit/f7659b9bd59d3eec0751309d617a07c73669bf02 Exception: ``` java.lang.StackOverflowError at com.intellij.openapi.progress.Cancellation.currentJob(Cancellation.java:26) at com.intellij.openapi.progress.Cancellation.checkCancelled(Cancellation.java:35) at com.intellij.openapi.progress.impl.CoreProgressManager.doCheckCanceled(CoreProgressManager.java:133) at com.intellij.openapi.progress.ProgressManager.checkCanceled(ProgressManager.java:231) at com.intellij.openapi.progress.ProgressIndicatorProvider.checkCanceled(ProgressIndicatorProvider.java:23) at com.intellij.psi.impl.source.tree.CompositeElement.getPsi(CompositeElement.java:676) at com.intellij.psi.impl.source.SourceTreeToPsiMap.treeElementToPsi(SourceTreeToPsiMap.java:15) at com.intellij.psi.impl.source.tree.SharedImplUtil.getParent(SharedImplUtil.java:33) at com.intellij.extapi.psi.ASTWrapperPsiElement.getParent(ASTWrapperPsiElement.java:19) at org.arend.psi.ext.ArendCompositeElementKt.getTopmostEquivalentSourceNode(ArendCompositeElement.kt:88) at org.arend.psi.ext.ArendSourceNodeImpl.getTopmostEquivalentSourceNode(ArendCompositeElement.kt:123) at org.arend.psi.ext.ArendCompositeElementKt.getParentSourceNode(ArendCompositeElement.kt:109) at...