WIP: Avoid inG when possible
This is a proposal for how we might be able to avoid using inG
when just dealing with constant functors, which is the common case. The approach here is preferable because when defining your resources like
Definition one_shotΣ : gFunctors := #[GFunctor one_shotR].
you have no way to accidentally write down a recursive functor, and when you then later use subG one_shotΣ Σ
you are also not silently introducing any extra assumptions. (Cases of accidentally introduced assumptions include authG
assuming something is a discrete CMRA, or savedAnythingG
assuming something is a contractive functor.)
I ported just a few users to see if the approach is viable, and it seems it is. I added a closed proof for some code that actually uses resources, because it seems so far the only test case for that situation is in iris-examples. This also shows that the change is backwards-compatible, we don't have to port everything as once. To find places where we are still using the old pattern, just grep for inG
. Before I go on porting more things, I'd like to get some feedback.
Fixes #227