Skip to content

More suggestive error message for `iInv`.

Robbert Krebbers requested to merge robbert/iInv_error into master

See the discussion at https://mattermost.mpi-sws.org/iris/pl/x1q7ti6pxj857drboxnhecckwr

The error message is not fantastic, since invariants could also be opened around other (custom) modalities (in a custom logic) provided one has the right type class instances. I am not sure what to do about that.

Merge request reports