An error occurred while fetching folder content.
Forked from
Iris / Iris
Source project has a limited visibility.
Robbert Krebbers
authored
We used to normalize the goal, and then checked whether it was of a certain shape. Since `uPred_valid P` normalized to `True ⊢ P`, there was no way of making a distinction between the two, hence `True ⊢ P` was treated as `uPred_valid P`. In this commit, I use type classes to check whether the goal is of a certain shape. Since we declared `uPred_valid` as `Typeclasses Opaque`, we can now make a distinction between `True ⊢ P` and `uPred_valid P`.
Name | Last commit | Last update |
---|