Skip to content

big_sepM2 and associated lemmas

Dan Fruminrequested to merge
dfrumin/iris-coq:robbert/big_sepM2 into master

Following big_sepL2 and big_sepM. Based on some code from @robbertkrebbers.

Would like to hear your comments and also add some helpful lemmas about this big op.

Edited by Dan Frumin

Merge request reports