intellij-arend
intellij-arend copied to clipboard
Bug: removing import doesn't lead to error
- Have the following code:
\import Algebra.Monoid
\import Arith.Nat
\func lemma (n : Nat) : 0 + n = n => zro-left
- Remove the second import.
Expected: Arend shows "Cannot infer instance" error for zro-left
.
Actual: no errors are shown. Re-running type checking via gutter icon doesn't fix the issue. The only way to fix it is to close the project and open it again.