intellij-arend

intellij-arend copied to clipboard

Such documentation could be useful for people learning Arend. As an example, we could show [documentation for lemmas](https://arend-lang.github.io/documentation/language-reference/definitions/functions#lemmas) when users hower the mouse over `\lemma` here: ```tex \func \infixl 3...

marat-rkh

Redundant parentheses are not reported in the following code: ``` \func foo (F : Nat -> \Type) => (F 0) -> (F 0) ```

valis

In the following code, parentheses are redundant: ``` \func bar {x : \Sigma Nat Nat} => x.1 \func foo => bar {(1,2)} ```

valis

In this example, the caret is placed like this: `{?(foldr-monoid)}`. As you can see, there is no "Fill goal" in the context menu. To invoke it, I need to place...

marat-rkh

"Extend selection" doesn't properly work in equational reasoning

4

Consider the following code: ```agda \func +-swap (m n p : Nat) : m + (n + p) = n + (m + p) => m + (n + p)...

marat-rkh

"Split atomic pattern" for let expressions

2

```tex \func lemma1 => (1, 2) \func lemma2 : Nat => \let p => lemma1 \in {?} ``` "Split atomic pattern" could be suggested for `p` here.

marat-rkh

```tex \func lemma (p : ∃ {x} (x = 0)) : ∃ {x} (x = 1) => TruncP.map p (\lam q => {?}) ``` Since Arend 1.7 "Split atomic pattern"...

marat-rkh

Warn about partially applied infix operators in prefix form

2

https://arend-lang.github.io/documentation/language-reference/definitions/#infix-operators According to this section of the documentation, the following 2 usages of `+` are equivalent: ```tex \func f => map (3 +) [] \func g => map (+ 3)...

marat-rkh

Intentions are not working properly for goals with arguments

1

At least, "Replace with constructors" is among them. 

knisht

```tex \func f \alias {-caret-} => {?} ``` Call completion at `{-caret-}`, type `\`. There will be no `\infix` in the completion, but it is valid to use it there.

marat-rkh