Consistently write `TCOr (Affine ..) (Absorbing ..)` instead of the other way around. (!910) · Merge requests · Iris / Iris

Robbert Krebbers requested to merge robbert/tcor_affine_absorbing into master Apr 25, 2023

While working on !881 (merged), I noticed that in always all cases we write TCOr (Affine ..) (Absorbing ..) but in some it's the other way around. This is annoying when derived lemmas with a TCOr premise from another, since you have to destruct the TCOr.

This MR fixes the inconsistency.

Consistently write `TCOr (Affine ..) (Absorbing ..)` instead of the other way around.

Merge request reports