Potentially add Frame instances for all our Fractional instances
In !739 (merged) we have removed the general frame_fractional
instance and replaced it by connection-specific framing instances such as:
Global Instance frame_mapsto p l v q1 q2 RES :
FrameFractionalHyps p (l ↦{#q1} v) (λ q, l ↦{#q} v)%I RES q1 q2 →
Frame p (l ↦{#q1} v) (l ↦{#q2} v) RES | 5.
This is useful since it matches on the head symbol of the framed expression, which is a lot more efficient than frame_fractional
.
However, we have more Fractional
instances in the codebase, which for now do not support framing any more:
Fractional (λ q, mono_nat_auth_own γ q n)
Fractional (λ q, gset_bij_own_auth γ (DfracOwn q) L)
-
Fractional (λ q, k ↪[γ]{#q} v)
(forghost_map
) Fractional (λ q, ghost_map_auth γ q m)
Fractional (λ q, ghost_var γ q a)
Fractional (cinv_own γ)
If the need comes up, we should add them back. Also, if it was easier to add them (e.g. with some kind of macro), there'd be less hesitation to add these instances everywhere.