Skip to content

strengthen cmra_op_discrete

Ralf Jung requested to merge ralf/cmra-op-discrete into master

The cmra_op_discrete lemma is entirely unused so far from what I can tell. @jtassaro is using a variant of it in Perennial, but it turns out the lemma needs to be strengthened a bit to fit. This MR upstreams the strengthened version.

I preserved the original statement as cmra_op_discrete', but honestly I doubt that it is worth keeping. So @robbertkrebbers if you're fine with that I'd just remove it.

Merge request reports