Commit e6084d75 authored by Robbert Krebbers's avatar Robbert Krebbers

Regression test for issue #55.

parent 037f7e3f
......@@ -303,6 +303,14 @@ Lemma test_iNext_plus_3 P Q n m k :
^m ^(2 + S n + k) P - ^m ^(2 + S n) Q - ^k ^(S (S n + S m)) (P Q).
Proof. iIntros "H1 H2". iNext. iNext. iNext. iFrame. Qed.
Lemma test_iNext_unfold P Q n m (R := (^n P)%I) :
R ^m True.
Proof.
iIntros "HR". iNext.
match goal with |- context [ R ] => idtac | |- _ => fail end.
done.
Qed.
Lemma test_iEval x y : (y + x)%nat = 1 - S (x + y) = 2%nat : uPred M.
Proof.
iIntros (H).
......
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