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

Tests.

parent 2bea47fc
......@@ -396,6 +396,29 @@ No applicable tactic.
"HQ" : Q
--------------------------------------∗
▷ P ∗ Q
"test_iRevert_pure"
: string
1 goal
PROP : bi
φ : Prop
P : PROP
============================
"H" : <affine> ⌜φ⌝ -∗ P
--------------------------------------∗
<affine> ⌜φ⌝ -∗ P
"test_iRevert_pure_affine"
: string
1 goal
PROP : bi
BiAffine0 : BiAffine PROP
φ : Prop
P : PROP
============================
"H" : ⌜φ⌝ -∗ P
--------------------------------------∗
⌜φ⌝ -∗ P
"elim_mod_accessor"
: string
1 goal
......
......@@ -1146,6 +1146,22 @@ Proof.
iIntros (?) "HP HQ". iModIntro. Show. by iFrame.
Qed.
Check "test_iRevert_pure".
Lemma test_iRevert_pure (φ : Prop) P :
φ (<affine> φ - P) - P.
Proof.
(* Check that iRevert creates a wand instead of an implication *)
iIntros (Hφ) "H". iRevert (Hφ). Show. done.
Qed.
Check "test_iRevert_pure_affine".
Lemma test_iRevert_pure_affine `{!BiAffine PROP} (φ : Prop) P :
φ ( φ - P) - P.
Proof.
(* If the BI is affine, no affine modality should be added *)
iIntros (Hφ) "H". iRevert (Hφ). Show. done.
Qed.
End tests.
Section parsing_tests.
......
Supports Markdown
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