Bug: "Replace with constructor" removes code after hole

[marat-rkh]

\open Nat (+)

\func example : Nat => {?} + {?}

Call "Replace with constructor" on the first hole, select "zero", press Enter.

Expected:

\func example : Nat => zero + {?}

Actual:

\func example : Nat => zero

As you can see, + {?} was removed, which is incorrect.

[valis]

It's a bug in BasePass. At line 195 we pass expr.textRange to replaceExprSmart, but that's incorrect since we need to compute the actual deleted range. I think this functionality was already implemented in https://github.com/JetBrains/intellij-arend/pull/281. So, we need to wait until it's merged.

[marat-rkh]

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