Skip to content

if instances for absorbing, affine and persistent

Alix Trieu requested to merge atrieu/iris:if_instances into master

I added instances of the form

Global Instance if_persistent P Q (b: bool) : Persistent P -> Persistent Q -> Persistent (if b then P else Q).

for Absorbing, Affine and Persistent.

I only had to use the Persistent one in a development I worked on, but I figured the other instances might be useful too, so I added them.

Merge request reports