Marat Khabibullin

Not sure if it clarifies anything, but it seems like the bug happens after I use actions like "Replace with constructor" or "Fill goal".

This is true, according to the [Wikipedia article](https://en.wikipedia.org/wiki/List_of_logic_symbols) it is 00AC. Would it make sense to just allow any unicode symbols in aliases? Are there any technical challenges there?

Stumbled upon a similar issue while rewriting PLFA on Arend. The "Transitivity" section in [Relactions](https://plfa.github.io/Relations/) chapter demonstrates the following proof: ```Agda ≤-trans : ∀ {m n p : ℕ} →...

Yes, I think so.

Yeah, I use it. I believe type hints might be more convenient when you mostly read code. Selecting and invoking the action for each clause is too tedious.

Oh, I see. That could be a problem, indeed.

Same could be done for names in clauses:

Yes, I am, on a part- time basis) > This is because how expressions are parsed. They are BinOpSequence in the Psi syntax. But as far as I understand, it...

`org.arend.util.ArendBinOpUtilsKt#getBounds` might help with this issue.

No, I would implement it as an inspection with quick fixes in the plugin)