From 3fa2232a18565ad7db8a052d1de8f85d3146e804 Mon Sep 17 00:00:00 2001
From: Jonas Kastberg Hinrichsen <jkas@itu.dk>
Date: Tue, 30 Apr 2019 10:50:05 +0200
Subject: [PATCH] Introduced new notation for stypes

---
 theories/encodings/branching.v       |  8 +++---
 theories/encodings/stype.v           | 27 +++++++++---------
 theories/encodings/stype_enc.v       | 20 ++++++++++---
 theories/examples/branching_proofs.v |  5 ++--
 theories/examples/proofs.v           | 42 ++++++++++------------------
 theories/examples/proofs_enc.v       | 36 ++++++++----------------
 theories/typing/stype.v              | 19 +++++++++++--
 7 files changed, 79 insertions(+), 78 deletions(-)

diff --git a/theories/encodings/branching.v b/theories/encodings/branching.v
index b422bde..f0ce12e 100644
--- a/theories/encodings/branching.v
+++ b/theories/encodings/branching.v
@@ -40,8 +40,8 @@ Section DualBranch.
 End DualBranch.
 Global Typeclasses Opaque TSB.
 
-Notation TSelect := (TSB Send).
-Notation TBranch := (TSB Receive).
+Infix "<+>" := (TSB Send) (at level 85) : stype_scope.
+Infix "<&>" := (TSB Receive) (at level 85) : stype_scope.
 
 Section branching_specs.
   Context `{!heapG Σ} (N : namespace).
@@ -58,7 +58,7 @@ Section branching_specs.
       else "b2".
 
   Lemma select_st_spec st1 st2 γ c s (b : bool) :
-    {{{ ⟦ c @ s : TSelect st1 st2 ⟧{N,γ} }}}
+    {{{ ⟦ c @ s : st1 <+> st2 ⟧{N,γ} }}}
       select c #s #b
     {{{ RET #(); ⟦ c @ s : (if b then st1 else st2) ⟧{N,γ} }}}.
   Proof.
@@ -72,7 +72,7 @@ Section branching_specs.
   Qed.
 
   Lemma branch_st_spec st1 st2 γ c s (b1 b2 : val) Φ :
-    ⟦ c @ s : TBranch st1 st2 ⟧{N,γ} -∗
+    ⟦ c @ s : st1 <&> st2 ⟧{N,γ} -∗
     (⟦ c @ s : st1 ⟧{N,γ} -∗ (Φ b1)) -∗
     (⟦ c @ s : st2 ⟧{N,γ} -∗ (Φ b2)) -∗
     WP branch c #s b1 b2 {{ v, Φ v }}.
diff --git a/theories/encodings/stype.v b/theories/encodings/stype.v
index 37fb923..0129edf 100644
--- a/theories/encodings/stype.v
+++ b/theories/encodings/stype.v
@@ -75,7 +75,7 @@ Section stype_interp.
     match vs with
     | [] => st1 ≡ dual_stype st2
     | v::vs => match st2 with
-               | TReceive P st2  => P v ∗ st_eval vs st1 (st2 v)
+               | TSR Receive P st2  => P v ∗ st_eval vs st1 (st2 v)
                | _ => False
                end
     end%I.
@@ -109,7 +109,7 @@ Section stype_interp.
   Qed.
 
   Lemma st_eval_send (P : val -> iProp Σ) st l str v :
-    P v -∗ st_eval l (TSend P st) str -∗ st_eval (l ++ [v]) (st v) str.
+    P v -∗ st_eval l (TSR Send P st) str -∗ st_eval (l ++ [v]) (st v) str.
   Proof.
     iIntros "HP".
     iRevert (str).
@@ -128,7 +128,7 @@ Section stype_interp.
   Qed.
 
   Lemma st_eval_recv (P : val → iProp Σ) st1 l st2 v :
-     st_eval (v :: l) st1 (TReceive P st2) -∗ st_eval l st1 (st2 v) ∗ P v.
+     st_eval (v :: l) st1 (TSR Receive P st2) -∗ st_eval l st1 (st2 v) ∗ P v.
   Proof. iDestruct 1 as "[HP Heval]". iFrame. Qed.
 
   Definition inv_st (γ : st_name) (c : val) : iProp Σ :=
@@ -166,9 +166,9 @@ Section stype_interp.
   Qed.
 End stype_interp.
 
-  Notation "⟦ c @ s : sτ ⟧{ N , γ }" := (interp_st N γ sτ c s)
-    (at level 10, s at next level, sτ at next level, γ at next level,
-     format "⟦  c  @  s  :  sτ  ⟧{ N , γ }").
+Notation "⟦ c @ s : st ⟧{ N , γ }" := (interp_st N γ st c s)
+  (at level 10, s at next level, st at next level, γ at next level,
+   format "⟦  c  @  s  :  st  ⟧{ N , γ }").
 
 Section stype_specs.
   Context `{!heapG Σ} (N : namespace).
@@ -221,7 +221,7 @@ Section stype_specs.
 
   Lemma send_vs c γ s (P : val → iProp Σ) st E :
     ↑N ⊆ E →
-    ⟦ c @ s : TSend P st ⟧{N,γ} ={E,E∖↑N}=∗
+    ⟦ c @ s : TSR Send P st ⟧{N,γ} ={E,E∖↑N}=∗
       ∃ vs, chan_own (st_c_name γ) s vs ∗
       ▷ (∀ v, P v -∗
               chan_own (st_c_name γ) s (vs ++ [v])
@@ -273,11 +273,12 @@ Section stype_specs.
           iApply (st_eval_send with "HP").
             by iRewrite -"Heq".
       }
+
       iModIntro. iFrame. rewrite /is_st. auto.
   Qed.
 
   Lemma send_st_spec st γ c s (P : val → iProp Σ) v :
-    {{{ P v ∗ ⟦ c @ s : TSend P st ⟧{N,γ} }}}
+    {{{ P v ∗ ⟦ c @ s : <!> @ P , st ⟧{N,γ} }}}
       send c #s v
     {{{ RET #(); ⟦ c @ s : st v ⟧{N,γ} }}}.
   Proof.
@@ -292,11 +293,11 @@ Section stype_specs.
 
   Lemma try_recv_vs c γ s (P : val → iProp Σ) st E :
     ↑N ⊆ E →
-    ⟦ c @ s : TReceive P st ⟧{N,γ}
+    ⟦ c @ s : TSR Receive P st ⟧{N,γ}
     ={E,E∖↑N}=∗
       ∃ vs, chan_own (st_c_name γ) (dual_side s) vs ∗
       (▷ ((⌜vs = []⌝ -∗ chan_own (st_c_name γ) (dual_side s) vs ={E∖↑N,E}=∗
-           ⟦ c @ s : TReceive P st ⟧{N,γ}) ∧
+           ⟦ c @ s : TSR Receive P st ⟧{N,γ}) ∧
           (∀ v vs', ⌜vs = v :: vs'⌝ -∗
                chan_own (st_c_name γ) (dual_side s) vs' -∗ |={E∖↑N,E}=>
                ⟦ c @ s : (st v) ⟧{N,γ} ∗ ▷  P v))).
@@ -364,9 +365,9 @@ Section stype_specs.
   Qed.
 
   Lemma try_recv_st_spec st γ c s (P : val → iProp Σ) :
-    {{{ ⟦ c @ s : TReceive P st ⟧{N,γ} }}}
+    {{{ ⟦ c @ s : <?> @ P , st ⟧{N,γ} }}}
       try_recv c #s
-    {{{ v, RET v; (⌜v = NONEV⌝ ∧ ⟦ c @ s : TReceive P st ⟧{N,γ}) ∨
+    {{{ v, RET v; (⌜v = NONEV⌝ ∧ ⟦ c @ s : <?> @ P, st ⟧{N,γ}) ∨
                   (∃ w, ⌜v = SOMEV w⌝ ∧ ⟦ c @ s : st w ⟧{N,γ} ∗ ▷ P w)}}}.
   Proof.
     iIntros (Φ) "Hrecv HΦ".
@@ -393,7 +394,7 @@ Section stype_specs.
   Qed.
 
   Lemma recv_st_spec st γ c s (P : val → iProp Σ) :
-    {{{ ⟦ c @ s : TReceive P st ⟧{N,γ} }}}
+    {{{ ⟦ c @ s : <?> @ P ,  st ⟧{N,γ} }}}
       recv c #s
     {{{ v, RET v; ⟦ c @ s : st v ⟧{N,γ} ∗ P v}}}.
   Proof.
diff --git a/theories/encodings/stype_enc.v b/theories/encodings/stype_enc.v
index ccfc32c..4edc469 100644
--- a/theories/encodings/stype_enc.v
+++ b/theories/encodings/stype_enc.v
@@ -91,8 +91,20 @@ Section DualStypeEnc.
 
 End DualStypeEnc.
 
-Notation TSend := (TSR' Send).
-Notation TReceive := (TSR' Receive).
+Notation "<!> x @ P , st" :=
+  (TSR' Send (λ x, P%I) (λ x, st%stype))
+  (at level 200, x pattern, st at level 200) : stype_scope.
+Notation "<?> x @ P , st" :=
+  (TSR' Receive (λ x, P%I) (λ x, st%stype))
+  (at level 200, x pattern, st at level 200) : stype_scope.
+Notation "<!> x , st" := (<!> x @ True, (st x))%stype
+  (at level 200, x pattern, st at level 200) : stype_scope.
+Notation "<?> x , st" := (<?> x @ True, (st x))%stype
+  (at level 200, x pattern, st at level 200) : stype_scope.
+Notation "<!> @ P , st" := (<!> dummy__ @ P dummy__, st dummy__)%stype
+  (at level 200, st at level 200) : stype_scope.
+Notation "<?> @ P , st" := (<?> dummy__ @ P dummy__, st dummy__)%stype
+  (at level 200, st at level 200) : stype_scope.
 
 Section stype_enc_specs.
   Context `{!heapG Σ} (N : namespace).
@@ -100,7 +112,7 @@ Section stype_enc_specs.
 
   Lemma send_st_spec (A : Type) `{EncDec A}
         st γ c s (P : A → iProp Σ) w :
-    {{{ P w ∗ ⟦ c @ s : (TSend P st) ⟧{N,γ} }}}
+    {{{ P w ∗ ⟦ c @ s : <!> @ P, st ⟧{N,γ} }}}
       send c #s (encode w)
     {{{ RET #(); ⟦ c @ s : st w ⟧{N,γ} }}}.
   Proof.
@@ -116,7 +128,7 @@ Section stype_enc_specs.
 
   Lemma recv_st_spec (A : Type) `{EncDec A}
         st γ c s (P : A → iProp Σ) :
-    {{{ ⟦ c @ s : (TReceive P st) ⟧{N,γ} }}}
+    {{{ ⟦ c @ s : <?> @ P, st ⟧{N,γ} }}}
       recv c #s
     {{{ v, RET (encode v); ⟦ c @ s : st v ⟧{N,γ} ∗ P v }}}.
   Proof.
diff --git a/theories/examples/branching_proofs.v b/theories/examples/branching_proofs.v
index 1e6a739..5d80c1e 100644
--- a/theories/examples/branching_proofs.v
+++ b/theories/examples/branching_proofs.v
@@ -20,9 +20,8 @@ Section BranchingExampleProofs.
   Proof.
     iIntros (Φ H) "HΦ".
     rewrite /branch_example.
-    wp_apply (new_chan_st_spec N (TSelect
-                                    (TReceive (λ v, ⌜v = 5⌝%I) (λ v, TEnd))
-                                    TEnd))=> //;
+    wp_apply (new_chan_st_spec N
+      ((<?> v @ ⌜v = 5⌝, TEnd)  <+> (TEnd)))=> //;
     iIntros (c γ) "[Hstl Hstr]".
     wp_apply (select_st_spec with "Hstl");
     iIntros "Hstl".
diff --git a/theories/examples/proofs.v b/theories/examples/proofs.v
index e81c6bf..262c675 100644
--- a/theories/examples/proofs.v
+++ b/theories/examples/proofs.v
@@ -10,16 +10,12 @@ Section ExampleProofs.
   Context `{!heapG Σ} (N : namespace).
   Context `{!logrelG val Σ}.
 
-  Notation "⟦ c @ s : sτ ⟧{ γ }" := (interp_st N γ sτ c s)
-    (at level 10, s at next level, sτ at next level, γ at next level,
-     format "⟦  c  @  s  :  sτ  ⟧{ γ }").
-
   Lemma seq_proof :
     {{{ True }}} seq_example {{{ v, RET v; ⌜v = #5⌝ }}}.
   Proof.
     iIntros (Φ H) "HΦ".
     rewrite /seq_example.
-    wp_apply (new_chan_st_spec N (TSend (λ v, ⌜v = #5⌝%I) (λ v, TEnd)))=> //;
+    wp_apply (new_chan_st_spec N (<!> v @ ⌜v = #5⌝, TEnd))=> //;
     iIntros (c γ) "[Hstl Hstr]"=> /=.
     wp_apply (send_st_spec N with "[$Hstl //]");
     iIntros "Hstl".
@@ -33,7 +29,7 @@ Section ExampleProofs.
   Proof.
     iIntros (Φ H) "HΦ".
     rewrite /par_example.
-    wp_apply (new_chan_st_spec N (TSend (λ v, ⌜v = #5⌝%I) (λ v, TEnd)))=> //;
+    wp_apply (new_chan_st_spec N (<!> v @ ⌜v = #5⌝, TEnd))=> //;
     iIntros (c γ) "[Hstl Hstr]"=> /=.
     wp_apply (wp_fork with "[Hstl]").
     - iNext. wp_apply (send_st_spec N with "[$Hstl //]"). eauto.
@@ -49,13 +45,10 @@ Section ExampleProofs.
     iIntros (Φ H) "HΦ".
     rewrite /par_2_example.
     wp_apply (new_chan_st_spec N
-      (TSend
-        (λ v, ⌜v = #5⌝%I)
-        (λ v, TReceive
-                (λ v',
-                  (∃ w, ⌜v = LitV $ LitInt $ w⌝ ∧
-                   ∃ w', ⌜v' = LitV $ LitInt $ w' ∧ w' >= w+2⌝)%I)
-                (λ v', TEnd))))=> //;
+      (<!> v @ ⌜v = #5⌝,
+               <?> v' @ (∃ w, ⌜v = LitV $ LitInt $ w⌝ ∧
+                         ∃ w', ⌜v' = LitV $ LitInt $ w' ∧ w' >= w+2⌝),
+                        TEnd))=> //;
     iIntros (c γ) "[Hstl Hstr]"=> /=.
     wp_apply (wp_fork with "[Hstr]").
     - iNext.
@@ -80,8 +73,8 @@ Section ExampleProofs.
     iIntros (Φ H) "HΦ".
     rewrite /heaplet_example.
     wp_apply (new_chan_st_spec N
-      (TSend (λ v, (∃ l, ⌜v = LitV $ LitLoc $ l⌝ ∧ (l ↦ #5))%I)
-             (λ v, TEnd)))=> //;
+      (<!> v @ (∃ l, ⌜v = LitV $ LitLoc $ l⌝ ∧ (l ↦ #5)),
+               TEnd))=> //;
     iIntros (c γ) "[Hstl Hstr]"=> /=.
     wp_apply (wp_fork with "[Hstl]").
     - iNext.
@@ -102,12 +95,8 @@ Section ExampleProofs.
     iIntros (Φ H) "HΦ".
     rewrite /channel_example.
     wp_apply (new_chan_st_spec N
-      (TSend
-        (λ v, ∃ γ,
-          ⟦ v @ Right : (TReceive
-                           (λ v : val, ⌜v = #5⌝)
-                           (λ _ : val, TEnd)) ⟧{γ})%I
-        (λ v, TEnd)))=> //;
+      (<!> v @ (∃ γ, ⟦ v @ Right : <?> v @ ⌜v = #5⌝, TEnd ⟧{N,γ}),
+               TEnd))=> //;
     iIntros (c γ) "[Hstl Hstr]"=> /=.
     wp_apply (wp_fork with "[Hstl]").
     - iNext.
@@ -132,8 +121,7 @@ Section ExampleProofs.
   Proof.
     iIntros (Φ H) "HΦ".
     rewrite /bad_seq_example.
-    wp_apply (new_chan_st_spec N
-               (TSend (λ v, ⌜v = #5⌝%I) (λ v, TEnd)))=> //;
+    wp_apply (new_chan_st_spec N (<!> v @ ⌜v = #5⌝, TEnd))=> //;
     iIntros (c γ) "[Hstl Hstr]"=> /=.
     wp_apply (recv_st_spec _ with "Hstr");
     iIntros (v) "[Hstr HP]".
@@ -148,8 +136,7 @@ Section ExampleProofs.
   Proof.
     iIntros (Φ H) "HΦ".
     rewrite /bad_par_example.
-    wp_apply (new_chan_st_spec N
-               (TSend (λ v, ⌜v = #5⌝%I) (λ v, TEnd)))=> //;
+    wp_apply (new_chan_st_spec N (<!> v @ ⌜v = #5⌝, TEnd))=> //;
     iIntros (c γ) "[Hstl Hstr]"=> /=.
     wp_apply (wp_fork with "[Hstl]").
     - iNext. by wp_finish.
@@ -162,10 +149,9 @@ Section ExampleProofs.
   Proof.
     iIntros (Φ H) "HΦ".
     rewrite /bad_interleave_example.
-    wp_apply (new_chan_st_spec N (TSend (λ v, ⌜v = #5⌝%I) (λ v, TEnd)))=> //;
+    wp_apply (new_chan_st_spec N (<!> v @ ⌜v = #5⌝, TEnd))=> //;
     iIntros (c γ) "[Hstl Hstr]"=> /=.
-    wp_apply (new_chan_st_spec N
-               (TReceive (λ v, ⌜v = #5⌝%I) (λ v, TEnd)))=> //;
+    wp_apply (new_chan_st_spec N (<?> v @ ⌜v = #5⌝, TEnd))=> //;
     iIntros (c' γ') "[Hstl' Hstr']"=> /=.
     wp_apply (wp_fork with "[Hstr Hstr']").
     - iNext. wp_apply (recv_st_spec _ with "Hstr");
diff --git a/theories/examples/proofs_enc.v b/theories/examples/proofs_enc.v
index 8b943de..5dd0ba4 100644
--- a/theories/examples/proofs_enc.v
+++ b/theories/examples/proofs_enc.v
@@ -15,8 +15,7 @@ Section ExampleProofsEnc.
   Proof.
     iIntros (Φ H) "HΦ".
     rewrite /seq_example.
-    wp_apply (new_chan_st_spec N
-             (TSend (λ v, ⌜v = 5⌝%I) (λ v, TEnd)))=> //;
+    wp_apply (new_chan_st_spec N (<!> v @ ⌜v = 5⌝, TEnd))=> //;
     iIntros (c γ) "[Hstl Hstr]"=> /=.
     wp_apply (send_st_spec N Z with "[$Hstl //]");
     iIntros "Hstl".
@@ -35,11 +34,9 @@ Section ExampleProofsEnc.
     iIntros (Φ H) "HΦ".
     rewrite /par_2_example.
     wp_apply (new_chan_st_spec N
-      (TSend
-        (λ v:Z, ⌜5 ≤ v⌝%I)
-        (λ v:Z, TReceive
-                  (λ v':Z, ⌜v+2 ≤ v'⌝%I)
-                  (λ v':Z, TEnd))))=> //;
+      (<!> v @ ⌜5 ≤ v⌝,
+               <?> v' @ ⌜v+2 ≤ v'⌝,
+                        TEnd))=> //;
     iIntros (c γ) "[Hstl Hstr]"=> /=.
     wp_apply (wp_fork with "[Hstr]").
     - iNext.
@@ -62,9 +59,7 @@ Section ExampleProofsEnc.
   Proof.
     iIntros (Φ H) "HΦ".
     rewrite /heaplet_example.
-    wp_apply (new_chan_st_spec N
-      (TSend (λ v, (v ↦ #5)%I)
-             (λ v, TEnd)))=> //;
+    wp_apply (new_chan_st_spec N (<!> v @ (v ↦ #5), TEnd))=> //;
     iIntros (c γ) "[Hstl Hstr]"=> /=.
     wp_apply (wp_fork with "[Hstl]").
     - iNext.
@@ -85,16 +80,12 @@ Section ExampleProofsEnc.
     iIntros (Φ H) "HΦ".
     rewrite /channel_example.
     wp_apply (new_chan_st_spec N
-      (TSend (λ v, ∃ γ, ⟦ v @ Right :
-        (TReceive
-          (λ v, ⌜v = 5⌝)
-          (λ _, TEnd)) ⟧{N, γ})%I
-      (λ v, TEnd)))=> //;
+      (<!> v @ (∃ γ, ⟦ v @ Right : <?> v @ ⌜v = 5⌝, TEnd ⟧{N,γ}),
+               TEnd))=> //;
     iIntros (c γ) "[Hstl Hstr]"=> /=.
     wp_apply (wp_fork with "[Hstl]").
     - iNext.
-      wp_apply (new_chan_st_spec N
-        (TSend (λ v, ⌜v = 5⌝%I) (λ v, TEnd)))=> //;
+      wp_apply (new_chan_st_spec N (<!> v @ ⌜v = 5⌝, TEnd))=> //;
       iIntros (c' γ') "[Hstl' Hstr']"=> /=.
       wp_apply (send_st_spec N val with "[Hstl Hstr']");
         first by eauto 10 with iFrame.
@@ -116,8 +107,7 @@ Section ExampleProofsEnc.
   Proof.
     iIntros (Φ H) "HΦ".
     rewrite /bad_seq_example.
-    wp_apply (new_chan_st_spec N
-               (TSend (λ v, ⌜v = 5⌝%I) (λ v, TEnd)))=> //;
+    wp_apply (new_chan_st_spec N (<!> v @ ⌜v = 5⌝, TEnd))=> //;
     iIntros (c γ) "[Hstl Hstr]"=> /=.
     wp_apply (recv_st_spec N Z with "Hstr");
     iIntros (v) "[Hstr HP]".
@@ -133,8 +123,7 @@ Section ExampleProofsEnc.
   Proof.
     iIntros (Φ H) "HΦ".
     rewrite /bad_par_example.
-    wp_apply (new_chan_st_spec N
-               (TSend (λ v, ⌜v = 5⌝%I) (λ v, TEnd)))=> //;
+    wp_apply (new_chan_st_spec N (<!> v @ ⌜v = 5⌝, TEnd))=> //;
     iIntros (c γ) "[Hstl Hstr]"=> /=.
     wp_apply (wp_fork with "[Hstl]").
     - iNext. by wp_finish.
@@ -149,10 +138,9 @@ Section ExampleProofsEnc.
   Proof.
     iIntros (Φ H) "HΦ".
     rewrite /bad_interleave_example.
-    wp_apply (new_chan_st_spec N (TSend (λ v, ⌜v = 5⌝%I) (λ v, TEnd)))=> //;
+    wp_apply (new_chan_st_spec N (<!> v @ ⌜v = 5⌝, TEnd))=> //;
     iIntros (c γ) "[Hstl Hstr]"=> /=.
-    wp_apply (new_chan_st_spec N
-               (TReceive (λ v, ⌜v = 5⌝%I) (λ v, TEnd)))=> //;
+    wp_apply (new_chan_st_spec N (<?> v @ ⌜v = 5⌝, TEnd))=> //;
     iIntros (c' γ') "[Hstl' Hstr']"=> /=.
     wp_apply (wp_fork with "[Hstr Hstr']").
     - iNext. wp_apply (recv_st_spec _ with "Hstr");
diff --git a/theories/typing/stype.v b/theories/typing/stype.v
index d6e5d17..84f31e4 100644
--- a/theories/typing/stype.v
+++ b/theories/typing/stype.v
@@ -30,8 +30,23 @@ Fixpoint dual_stype {V A} (st : stype V A) :=
   end.
 Instance: Params (@dual_stype) 2.
 
-Notation TSend P st := (TSR Send P st).
-Notation TReceive P st := (TSR Receive P st).
+Delimit Scope stype_scope with stype.
+Bind Scope stype_scope with stype.
+
+Notation "<!> x @ P , st" :=
+  (TSR Send (λ x, P%I) (λ x, st%stype))
+  (at level 200, x pattern, st at level 200) : stype_scope.
+Notation "<?> x @ P , st" :=
+  (TSR Receive (λ x, P%I) (λ x, st%stype))
+  (at level 200, x pattern, st at level 200) : stype_scope.
+Notation "<!> x , st" := (<!> x @ True, (st x))%stype
+  (at level 200, x pattern, st at level 200) : stype_scope.
+Notation "<?> x , st" := (<?> x @ True, (st x))%stype
+  (at level 200, x pattern, st at level 200) : stype_scope.
+Notation "<!> @ P , st" := (<!> dummy__ @ P dummy__, st dummy__)%stype
+  (at level 200, st at level 200) : stype_scope.
+Notation "<?> @ P , st" := (<?> dummy__ @ P dummy__, st dummy__)%stype
+  (at level 200, st at level 200) : stype_scope.
 
 Section stype_ofe.
   Context {V : Type}.
-- 
GitLab