Marat Khabibullin
Marat Khabibullin
As you can see, it is not possible to use `¬` symbol as an alias. This symbol is used commonly for negation, it is a bit surprising that I cannot...
I was writing a proof, and at some point plugin stoped showing goals although I had a hole: As you can see `
According to the language reference ([here](https://arend-lang.github.io/documentation/language-reference/prelude)), many declarations in Prelude are treated in a special way, they are not usual language constructs. It would be nice to have documentation comments...
Hi! The section about Control Flow Graphs is not documented yet and I'm very interested in it. It would be great if you could add the information about basics of...
```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...
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...