Commit 8fa39f7c authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'minor-notation-cleanup' into 'master'

Use |-@{...} to avoid the need for casts (in tests)

See merge request !785
parents d7eae97a ac310b6a
Pipeline #64404 passed with stage
in 15 minutes and 10 seconds
......@@ -130,8 +130,7 @@ Ltac unseal := rewrite !unseal_eqs /=.
Section primitive.
Local Arguments siProp_holds !_ _ /.
Notation "P ⊢ Q" := (siProp_entails P Q)
(at level 99, Q at level 200, right associativity).
Notation "P ⊢ Q" := (siProp_entails P Q).
Notation "'True'" := (siProp_pure True) : siProp_scope.
Notation "'False'" := (siProp_pure False) : siProp_scope.
Notation "'⌜' φ '⌝'" := (siProp_pure φ%type%stdpp) : siProp_scope.
......
......@@ -865,7 +865,7 @@ Lemma test_specialize_intuitionistic P Q :
P - (P - Q) - Q.
Proof. iIntros "#HP #HQ". iSpecialize ("HQ" with "HP"). done. Qed.
Lemma test_iEval x y : (y + x)%nat = 1 - S (x + y) = 2%nat : PROP.
Lemma test_iEval x y : (y + x)%nat = 1 @{PROP} S (x + y) = 2%nat .
Proof.
iIntros (H).
iEval (rewrite (Nat.add_comm x y) // H).
......@@ -880,21 +880,21 @@ Proof.
Qed.
Check "test_iSimpl_in".
Lemma test_iSimpl_in x y : (3 + x)%nat = y - S (S (S x)) = y : PROP.
Lemma test_iSimpl_in x y : (3 + x)%nat = y @{PROP} S (S (S x)) = y .
Proof. iIntros "H". iSimpl in "H". Show. done. Qed.
Lemma test_iSimpl_in_2 x y z :
(3 + x)%nat = y - (1 + y)%nat = z -
S (S (S x)) = y : PROP.
(3 + x)%nat = y @{PROP} (1 + y)%nat = z -
S (S (S x)) = y .
Proof. iIntros "H1 H2". iSimpl in "H1 H2". Show. done. Qed.
Lemma test_iSimpl_in3 x y z :
(3 + x)%nat = y - (1 + y)%nat = z -
S (S (S x)) = y : PROP.
(3 + x)%nat = y @{PROP} (1 + y)%nat = z -
S (S (S x)) = y .
Proof. iIntros "#H1 H2". iSimpl in "#". Show. done. Qed.
Check "test_iSimpl_in4".
Lemma test_iSimpl_in4 x y : (3 + x)%nat = y - S (S (S x)) = y : PROP.
Lemma test_iSimpl_in4 x y : (3 + x)%nat = y @{PROP} S (S (S x)) = y .
Proof. iIntros "H". Fail iSimpl in "%". by iSimpl in "H". Qed.
Check "test_iRename".
......
......@@ -67,7 +67,7 @@ Section tests.
iStartProof. iIntros (n) "$".
Qed.
Lemma test_embed_wand (P Q : PROP) : (P - Q) - P - Q : monPred.
Lemma test_embed_wand (P Q : PROP) : (P - Q) @{monPredI} P - Q.
Proof.
iIntros "H HP". by iApply "H".
Qed.
......
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