[Iris-Club] CMRA structure on uPred

[Robbert Krebbers]

On 10/10/2016 09:29 PM, Ralf Jung wrote:
> This could be entirely separate from the algebraic hierarchy, and not
> increase it at all. (I think I saw this proposed somewhere, but can't
> find the source now, so here I'm just echoing someone else.)  I don't
> see a good reason why everything you compose with bigops should have a
> core and validity, and there are some things you can do already with
> just associativity -- tying this to RAs seems rather silly, and even
> prevents us from also doing e.g. bigops on conjunction.
That is what ssreflect is doing, see:

   https://hal.inria.fr/inria-00331193

I think I mentioned this to JH during a meeting lately, and yes, 
whenever I have some time again, I may refactor the big op stuff into 
something like what ssreflect is doing.