Commit bc947bd5 authored by Robbert Krebbers's avatar Robbert Krebbers

Test case for performance regression akin to #153.

Fixed by stdpp 93b4ec70e13a573a9055a5bf1269f5885e18e843.
parent e6084d75
......@@ -311,6 +311,10 @@ Proof.
done.
Qed.
Lemma test_iNext_fail P Q a b c d e f g h i j:
^(a + b) ^(c + d + e) P - ^(f + g + h + i + j) True.
Proof. iIntros "H". iNext. 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