Open
Description
Created by @mschwerhoff on 2017-04-20 12:15
Currently, Viper rejects assertions that nest perm under forperm, e.g.
forperm[f] r :: perm(r.f) == write ==> true
However, there doesn't seem to be a good reason for disallowing this. Hence, we should support it.