`IsOp` classes are poorly named, fulfill two functions, yet they will be used differently after !930
We noticed in !1004 that the IsOp
, IsOp'
and IsOpLR
classes are somewhat problematic.
Firstly, their names are somewhat confusing (something like IntoOp
is imo more descriptive of what IsOpLR
does).
Secondly, IsOp
is used both for merging (iCombine
ing owns) and splitting (iSplit
/iDestruct
ing owns) ops.
This usually saves some lines of code for clients, but complicates things in other cases.
This could be fixed, but these classes will also be used somewhat differently once !930 lands.
After !930, there will be an IsValidOp
class responsible for iCombine
ing.
The current proposal for !930 would still rely on IsOp
---but only for some cmra
s (those with trivial validity),
and only for cmra
s that occur as 'leaves' in a term (so not for cmra
s constructed with combinators).