Marat Khabibullin
Marat Khabibullin
```tex \func def \alias defalias (n : Nat) : Nat | 0 => 0 | suc n => defalias n \func usage => defalias ``` 1. Put the caret at...
 Project SDK is needed if you want to create a language extension or debug typechecking. It would be nice to add this information to the UI, say, it the...
In Emacs mode for Coq, we can view the diff between expected and actual types in typechecking errors. This could be useful when types are large and it is not...
In Emacs mode for Coq (with company-coq), there is a special mode that shows math symbols instead of some language constructions, like lambdas, `forall` quantifier, etc. With prettify-symbols-mode off: With...
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...
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...
Consider the following code: ```agda \func +-swap (m n p : Nat) : m + (n + p) = n + (m + p) => m + (n + p)...
```tex \func lemma1 => (1, 2) \func lemma2 : Nat => \let p => lemma1 \in {?} ``` "Split atomic pattern" could be suggested for `p` here.
```tex \func lemma (p : ∃ {x} (x = 0)) : ∃ {x} (x = 1) => TruncP.map p (\lam q => {?}) ``` Since Arend 1.7 "Split atomic pattern"...
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)...