Commit 5f74d09c authored by Robbert Krebbers's avatar Robbert Krebbers Committed by Jacques-Henri Jourdan

Strip laters below ■ and □.

parent 2ca5469a
......@@ -932,6 +932,13 @@ Global Instance into_laterN_exist {A} n (Φ Ψ : A → PROP) :
IntoLaterN' n ( x, Φ x) ( x, Ψ x).
Proof. rewrite /IntoLaterN' /IntoLaterN -laterN_exist_2=> ?. by apply exist_mono. Qed.
Global Instance into_later_bare n P Q :
IntoLaterN n P Q IntoLaterN n ( P) ( Q).
Proof. rewrite /IntoLaterN=> ->. by rewrite laterN_bare_2. Qed.
Global Instance into_later_persistently n P Q :
IntoLaterN n P Q IntoLaterN n ( P) ( Q).
Proof. rewrite /IntoLaterN=> ->. by rewrite laterN_persistently. Qed.
Global Instance into_laterN_sep_l n P1 P2 Q1 Q2 :
IntoLaterN' n P1 Q1 IntoLaterN n P2 Q2
IntoLaterN' n (P1 P2) (Q1 Q2) | 10.
......
......@@ -217,6 +217,11 @@ Lemma test_iIntros_let P :
Q, let R := emp%I in P - R - Q - P Q.
Proof. iIntros (Q R) "$ _ $". Qed.
Lemma test_foo P Q : (Q P) - Q - P.
Proof.
iIntros "#HPQ HQ". iSplit; first done. iNext. by iRewrite "HPQ" in "HQ".
Qed.
Lemma test_iIntros_modalities `(!Absorbing P) :
( x : nat, x = 0 x = 0 - False - P - P)%I.
Proof.
......@@ -224,4 +229,5 @@ Proof.
iIntros "* **". (* Test that fast intros do not work under modalities *)
iIntros ([]).
Qed.
End tests.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment