Skip to content

Add pair_op_1 and pair_op_2

Dmitry Khalanskiy requested to merge dkhalanskiyjb/iris:pair_op_n into master

The two new lemmas allow splitting the resources in one component of a pair when the other component has nothing. In combination with pair_split, they allow to arbitrarily split the resource (a ⋅ a', b ⋅ b').

This is in line with prod_local_update_1 and prod_local_update_2, the lemmas that allow, in a sense, to only consider one component of a pair.

This change was not discussed earlier, I just needed these lemmas in my own developments.

Merge request reports