Commit bfe7dd4c authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Add test for iLöb.

parent 646bfc85
...@@ -162,6 +162,12 @@ Proof. iIntros "#?". by iSplit. Qed. ...@@ -162,6 +162,12 @@ Proof. iIntros "#?". by iSplit. Qed.
Lemma test_iSpecialize_persistent P Q : Lemma test_iSpecialize_persistent P Q :
P - ( P - Q) - Q. P - ( P - Q) - Q.
Proof. iIntros "#HP HPQ". by iSpecialize ("HPQ" with "HP"). Qed. Proof. iIntros "#HP HPQ". by iSpecialize ("HPQ" with "HP"). Qed.
Lemma test_iLöb P : ( n, ^n P)%I.
Proof.
iLöb as "IH". iDestruct "IH" as (n) "IH".
by iExists (S n).
Qed.
End tests. End tests.
Section more_tests. Section more_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