intellij-arend
intellij-arend copied to clipboard
JetBrains
Arend plugin for IntelliJ IDEA
Arend's PSI tree is in fact a CST, not an AST. It results in a lot off difficulties with this tree: there are some strange nodes like `ArendAtomFieldAcc`, and the...
``` \class Ring (E : \Set) | \infixl 6 + : E -> E -> E | \infixl 7 * : E -> E -> E \func test {R :...
After using the tracer the status of the definition is reset to untypecheked it seems.
```tex \open Nat (+) \func example : Nat => {?} + {?} ``` Call "Replace with constructor" on the first hole, select "zero", press Enter. Expected: ```tex \func example :...
1. Open the editor and paste the following `foo` function: 2. Notice, it has an implicit goal, but it is not shown in the Arend Messages. 3. There is no...
```tex \func foo => bar Nat nil \where { \func bar (A : \Type) (l : List A) => l } ``` Call `Change Argument Explicitness` on `(A : \Type)`,...
Here at line 724 I have accidentally introduced `{B : Type}` which shadows `B` in the pattern on the left side of `=>`. This lead to strange issues with implicit...
``` \func foo : Nat -> Nat => {?} \func bar => foo(1) ``` Yes, I know, it's a dumb case. Still the space should be inserted.
Suppose I am writing the following declaration: ```tex \data Term | ref Id | lam Id Term | app \alias \infixl 7 {-caret-} Term Term ``` I want to add...