program_logic/boxes.v · 5d66333ca9544f71d2b59cd6901e8dd8cb493287 · Simcha van Collem / Iris

Forked from Iris / Iris

Source project has a limited visibility.

8 years ago

Make f_equiv slightly more robust. · 5d66333c

Now, for example, when having equiv (Some x) (Some y) it will
try to find a Proper whose range is an equiv before hitting the
eq instance. My hack is general enough that it works for Forall2,
dist, and so on, too.

5d66333c

History

Make f_equiv slightly more robust.

Robbert Krebbers authored 8 years ago

Now, for example, when having equiv (Some x) (Some y) it will
try to find a Proper whose range is an equiv before hitting the
eq instance. My hack is general enough that it works for Forall2,
dist, and so on, too.