intellij-arend icon indicating copy to clipboard operation
intellij-arend copied to clipboard

Bug: removing import doesn't lead to error

Open marat-rkh opened this issue 3 years ago • 0 comments

  1. Have the following code:
\import Algebra.Monoid
\import Arith.Nat

\func lemma (n : Nat) : 0 + n = n => zro-left
  1. 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.

marat-rkh avatar Aug 25 '21 19:08 marat-rkh