intellij-arend
intellij-arend copied to clipboard
JetBrains
Arend plugin for IntelliJ IDEA
Import action may perform slow operations ``` java.lang.Throwable: Slow operations are prohibited on EDT. See SlowOperations.assertSlowOperationsAreAllowed javadoc. at com.intellij.openapi.diagnostic.Logger.error(Logger.java:182) at com.intellij.util.SlowOperations.assertSlowOperationsAreAllowed(SlowOperations.java:110) at com.intellij.util.indexing.FileBasedIndexImpl.ensureUpToDate(FileBasedIndexImpl.java:754) at com.intellij.psi.stubs.StubIndexImpl.getContainingIds(StubIndexImpl.java:501) at com.intellij.psi.stubs.StubIndexImpl.processElements(StubIndexImpl.java:305) at com.intellij.psi.stubs.StubIndex.getElements(StubIndex.java:100) at...
Consider the following code: ```tex \func foldr-append {A B : \Type} (** : A -> B -> B) (e : B) (xs ys : List A) : foldr ** e...
1. Have the following code: ```tex \import Algebra.Monoid \import Arith.Nat \func lemma (n : Nat) : 0 + n = n => zro-left ``` 2. Remove the second import. Expected:...
 Steps: 1. Have some declaration with a goal. 2. Open Arend Errors and check the line number (3 in this case). 3. Add a new line before the declaration....
Consider a declaration: Parameter name `d` is redundant here and can be replaced with `_`. This could simplify the declaration and improve readability as `_` stresses the fact that there...
Suppose I am defining a function: My caret is before the closing curly bracket. I know my code is incorrect, I need to write a type to fix it. **Expected**:...
As you can see, `=~` is a record, so it is a reference to a definition. Re-opening the project solves the issue. I encounter it from time to time, but...
Open `Equiv.ard` in `arend-lib` and call "Class Hierarchy" on `QEquiv`: I expect to see `sec` as implemented field, but it is not shown at all. Note that it works in...
Implement various quick fixes: - [x] All errors with WARNING_UNUSED level -- remove some part of the expression - [x] ArgumentExplicitnessError -- make explicit/implicit - [x] InstanceInferenceError (without classifying fields)...