Marat Khabibullin
Marat Khabibullin
```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.
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...
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...