program_logic/counter_examples.v · a095bb8af708a8b88fa219d1bafaef32123fe9c2 · Simcha van Collem / Iris

Forked from Iris / Iris

Source project has a limited visibility.

8 years ago

1.) iDestruct is able turns  into two implications (because uPred_iff
    is (type classes) transparent).
2.) iApply only backtracks on turning P  Q into P → Q or Q → P when
    there are no future premises. This is not the case for
    'P  □ (P → False)'.

a095bb8a

History

Remove FIXME.

Robbert Krebbers authored 8 years ago

1.) iDestruct is able turns  into two implications (because uPred_iff
    is (type classes) transparent).
2.) iApply only backtracks on turning P  Q into P → Q or Q → P when
    there are no future premises. This is not the case for
    'P  □ (P → False)'.