Discardable camera improvements
Generalization
I think the variant of dfrac
that I implemented with !531 (merged) can be generalized to a "discardable-anything":
Inductive discardable (A: cmraT) :=
| DOwn : A → dfrac
| DDiscarded : dfrac
| DBoth : A → dfrac.
with validity something like
Instance discardable_valid (A: cmraT) : Valid (discardable A) := λ x,
match x with
| DOwn q => ✓ q
| DDiscarded => True
| DBoth q => exists p, ✓ (q ⋅ p)
end%Qc.
I think this should work... what I am not sure about is if this is useful.^^
discarded idea: option Qp
old After !531 (merged), the public interface of dfrac
can basically be described via a smart constructor that takes option Qp
-- in fact I am adding such a notation in !486 (merged). We can probably rephrase all the existing lemmas in terms of that single constructor, and @robbertkrebbers agrees that that would make a better interface.
Edited by Ralf Jung