intellij-arend
intellij-arend copied to clipboard
JetBrains
Arend plugin for IntelliJ IDEA
Suppose I have some function: `\func foo (n m : Nat) : Bool => {?}` Naturally, I first write its signature and leave `=> {?}` as a result, because I...
Consider the following function: ```agda \func -'+assoc (m n p : Nat): m -' n -' p = m -' (n + p) | m, n, 0 => [n-'0=n] (m...
Invoke "Fill goal" on the following code: Expected result: Actual result: Note that `` `qed `` lost its `` ` ``. Also the last `{?}` is after the `qed`, not...
1. Install IntelliJ Community 2020.3.3 and Arend plugin. 2. Clone Arend tutorial project (https://github.com/arend-lang/tutorial-code) and open it in the IDE. When IDE starts, it shows 2 errors: ``` 10:22 PM...
Pressing enter in the following code sends the expression to the beginning of the line. ``` \module M \where { \func foo (x : Nat) : Nat => {-caret-}\case x...
https://github.com/intellij-rust/intellij-rust/tree/master/src/main/kotlin/org/rust/ide/spelling
Navigation from source does not work for errors embedded in goals.
1. No gui controls in "Create new Arend project" window 2. Want to have smarter Run Configuration gui controls for typechecking arend definitions Want to have list of all definitions...
I modified `binariesDir: bla` in `arend.yaml`, and a new binary dir is created. But it's not marked as an excluded dir, and the old dir is still excluded. Should we...
``` 2020-10-03 09:37:43,806 [ 187489] ERROR - aemon.impl.PassExecutorService - Plugin to blame: Arend version: 1.4.1 2020-10-03 09:37:43,806 [ 187489] ERROR - aemon.impl.PassExecutorService - Last Action: EditorBackSpace 2020-10-03 09:37:43,806 [ 187489]...