valis
valis
Make a separate subsystem for resolving. Highlight and PsiReference.resolve should just invoke this subsystem.
Signature of functions defined in instances (and other functions) must be specified explicitly. It is possible to generate them automatically. This can be implemented as an intention. Before: ``` \class...
When "Goto declaration or usages" (i.e., ctrl+click) is invoked on a declaration, it should show all of its usages, but this does not work in Arend.
Implicit arguments can be substituted with `?x`, where `x` is the name of the argument. Also, if the expression is type-checked, then the argument can be substituted with the inferred...
The signature of \use \level definitions is non-trivial, but it can be generated completely automatically.
This behavior should be configurable.
``` java.lang.NullPointerException at org.arend.intention.SplitAtomPatternIntention.getElementType(SplitAtomPatternIntention.kt:161) at org.arend.intention.SplitAtomPatternIntention.isApplicableTo(SplitAtomPatternIntention.kt:62) at org.arend.intention.SelfTargetingIntention.getTarget(SelfTargetingIntention.kt:62) at org.arend.intention.SelfTargetingIntention.isAvailable(SelfTargetingIntention.kt:78) at com.intellij.codeInsight.intention.impl.ShowIntentionActionsHandler.availableFor(ShowIntentionActionsHandler.java:169) at com.intellij.codeInsight.daemon.impl.ShowIntentionsPass.lambda$getActionsToShow$1(ShowIntentionsPass.java:339) at com.intellij.codeInsight.intention.impl.ShowIntentionActionsHandler.chooseBetweenHostAndInjected(ShowIntentionActionsHandler.java:202) at com.intellij.codeInsight.daemon.impl.ShowIntentionsPass.getActionsToShow(ShowIntentionsPass.java:338) at com.intellij.codeInsight.daemon.impl.ShowIntentionsPass.doCollectInformation(ShowIntentionsPass.java:242) at com.intellij.codeHighlighting.TextEditorHighlightingPass.collectInformation(TextEditorHighlightingPass.java:56) at com.intellij.codeInsight.daemon.impl.PassExecutorService$ScheduledPass.lambda$doRun$1(PassExecutorService.java:419) at com.intellij.openapi.application.impl.ApplicationImpl.tryRunReadAction(ApplicationImpl.java:1152) at com.intellij.codeInsight.daemon.impl.PassExecutorService$ScheduledPass.lambda$doRun$2(PassExecutorService.java:412) at com.intellij.openapi.progress.impl.CoreProgressManager.lambda$executeProcessUnderProgress$12(CoreProgressManager.java:608)...
For example, `field` is not completed in the following code: ``` \record R (field : Nat) \func axsax => ∃ (r : R) (r.field = 0) ```