removing `@

share/steel/examples/pulse/CustomSyntax.fst

@@ -343,16 +343,16 @@ fn sum2 (r:ref nat) (n:nat)
 
 ```pulse
 fn if_then_else_in_specs (r:ref U32.t)
-  requires `@(if true
+  requires (if true
               then pts_to r 0ul
               else pts_to r 1ul)
-  ensures  `@(if true
+  ensures  (if true
               then pts_to r 1ul
               else pts_to r 0ul)
 {
   // need this for typechecking !r on the next line,
   //   with inference of implicits
-  rewrite `@(if true then pts_to r 0ul else pts_to r 1ul)
+  rewrite (if true then pts_to r 0ul else pts_to r 1ul)
        as (pts_to r 0ul);
   let x = !r;
   r := U32.add x 1ul

share/steel/examples/pulse/bug-reports/DependentTuples.fst

@@ -24,7 +24,7 @@ fn tuple ()
   unfold exists_n global_tup._1;  // this unfold affects the type of the dependent 
                                   // tuple, so we lost syntactic equality and the 
                                   // following assertion fails
-  assert (`@(exists* n. pts_to global_tup._1 n));
+  assert ((exists* n. pts_to global_tup._1 n));
   admit()
 }
 ```

share/steel/examples/pulse/dice/cbor/CBOR.Pulse.fst

@@ -229,8 +229,8 @@ ensures
                     pts_to pi1 i1 ** pts_to pi2 i2 ** pts_to pdone done ** pts_to pres res **
                     cbor_array_iterator_match p1 i1 l1 **
                     cbor_array_iterator_match p2 i2 l2 **
-                    `@(cbor_array_iterator_match p1 i1 l1 @==> raw_data_item_match p1 a1 v1) **
-                    `@(cbor_array_iterator_match p2 i2 l2 @==> raw_data_item_match p2 a2 v2) **
+                    (cbor_array_iterator_match p1 i1 l1 @==> raw_data_item_match p1 a1 v1) **
+                    (cbor_array_iterator_match p2 i2 l2 @==> raw_data_item_match p2 a2 v2) **
                     pure (
                         List.Tot.length l1 == List.Tot.length l2 /\
                         Cbor.cbor_compare v1 v2 == (if res = 0s then Cbor.cbor_compare_array l1 l2 else I16.v res) /\
@@ -307,8 +307,8 @@ ensures
                     pts_to pi1 i1 ** pts_to pi2 i2 ** pts_to pdone done ** pts_to pres res **
                     cbor_map_iterator_match p1 i1 l1 **
                     cbor_map_iterator_match p2 i2 l2 **
-                    `@(cbor_map_iterator_match p1 i1 l1 @==> raw_data_item_match p1 a1 v1) **
-                    `@(cbor_map_iterator_match p2 i2 l2 @==> raw_data_item_match p2 a2 v2) **
+                    (cbor_map_iterator_match p1 i1 l1 @==> raw_data_item_match p1 a1 v1) **
+                    (cbor_map_iterator_match p2 i2 l2 @==> raw_data_item_match p2 a2 v2) **
                     pure (
                         List.Tot.length l1 == List.Tot.length l2 /\
                         (Cbor.cbor_compare v1 v2 == (if res = 0s then Cbor.cbor_compare_map l1 l2 else I16.v res)) /\
@@ -337,8 +337,8 @@ ensures
                         raw_data_item_match p2 (cbor_map_entry_value x2) (sndp v2') **
                         cbor_map_iterator_match p1 gi1' l1' **
                         cbor_map_iterator_match p2 gi2' l2' **
-                        `@((raw_data_item_map_entry_match p1 x1 v1' ** cbor_map_iterator_match p1 gi1' l1') @==> raw_data_item_match p1 a1 v1) **
-                        `@((raw_data_item_map_entry_match p2 x2 v2' ** cbor_map_iterator_match p2 gi2' l2') @==> raw_data_item_match p2 a2 v2) **
+                        ((raw_data_item_map_entry_match p1 x1 v1' ** cbor_map_iterator_match p1 gi1' l1') @==> raw_data_item_match p1 a1 v1) **
+                        ((raw_data_item_map_entry_match p2 x2 v2' ** cbor_map_iterator_match p2 gi2' l2') @==> raw_data_item_match p2 a2 v2) **
                         pts_to pres res ** pure ((I16.v res <: int) == (if Cbor.cbor_compare (fstp v1') (fstp v2') <> 0 then Cbor.cbor_compare (fstp v1') (fstp v2') else Cbor.cbor_compare (sndp v1') (sndp v2')))
                     {
                         let test = cbor_compare (cbor_map_entry_value x1) (cbor_map_entry_value x2);
@@ -843,7 +843,7 @@ requires
     A.pts_to_range a (SZ.v lo) (SZ.v hi) c **
     SM.seq_list_match c l (raw_data_item_map_entry_match full_perm)
 returns res: bool
-ensures `@(exists* (c': Seq.seq cbor_map_entry) (l': list (Cbor.raw_data_item & Cbor.raw_data_item)).
+ensures (exists* (c': Seq.seq cbor_map_entry) (l': list (Cbor.raw_data_item & Cbor.raw_data_item)).
     // FIXME: WHY WHY WHY do I need to use exists_ instead of Pulse exists? Error message is: "IOU"
     A.pts_to_range a (SZ.v lo) (SZ.v hi) c' **
     SM.seq_list_match c' l' (raw_data_item_map_entry_match full_perm) **

share/steel/examples/pulse/dice/cbor/CDDL.Pulse.fst

@@ -214,15 +214,15 @@ requires
     (
             R.pts_to pi i' **
             cbor_array_iterator_match p i' l' **
-            `@(cbor_array_iterator_match p i' l' @==> cbor_array_iterator_match p i l) **
+            (cbor_array_iterator_match p i' l' @==> cbor_array_iterator_match p i l) **
             pure (
                 opt_precedes (Ghost.reveal l) b /\
                 res == Some? (g l) /\
                 (res == true ==> Some?.v (g l) == l')
             )
     )
 ensures
-        `@(exists* i' l'.
+        (exists* i' l'.
             R.pts_to pi i' **
             cbor_array_iterator_match p i' l' **
             (cbor_array_iterator_match p i' l' @==> cbor_array_iterator_match p i l) **
@@ -290,7 +290,7 @@ fn impl_array_group3_item
         with gc i' l' . assert (
             raw_data_item_match p c gc **
             cbor_array_iterator_match p i' l' **
-            `@((raw_data_item_match p c gc ** cbor_array_iterator_match p i' l') @==> cbor_array_iterator_match p gi l)
+            ((raw_data_item_match p c gc ** cbor_array_iterator_match p i' l') @==> cbor_array_iterator_match p gi l)
         ); // this is needed for the explicit arguments to split_consume_l below
         let test = fty c;
         if (test) {
@@ -895,7 +895,7 @@ fn impl_matches_map_group_no_restricted
         pts_to pres res **
         pts_to pi i **
         cbor_map_iterator_match p i l **
-        `@(cbor_map_iterator_match p i l @==> raw_data_item_match p c v) **
+        (cbor_map_iterator_match p i l @==> raw_data_item_match p c v) **
         pure (
             list_ghost_forall_exists matches_map_group_entry' (Map?.v v) g.zero_or_more ==
                 (res && list_ghost_forall_exists matches_map_group_entry' l g.zero_or_more) /\
@@ -907,7 +907,7 @@ fn impl_matches_map_group_no_restricted
         let x = cbor_map_iterator_next pi;
         stick_trans ();
         let res = ig x;
-        with vx gi l . assert (pts_to pi gi ** raw_data_item_map_entry_match p x vx ** cbor_map_iterator_match p gi l ** `@((raw_data_item_map_entry_match p x vx ** cbor_map_iterator_match p gi l) @==> raw_data_item_match p c v)) ;
+        with vx gi l . assert (pts_to pi gi ** raw_data_item_map_entry_match p x vx ** cbor_map_iterator_match p gi l ** ((raw_data_item_map_entry_match p x vx ** cbor_map_iterator_match p gi l) @==> raw_data_item_match p c v)) ;
         stick_consume_l ()
             #(raw_data_item_map_entry_match p x vx)
             #(cbor_map_iterator_match p gi l);

share/steel/examples/pulse/dice/dpe/DPE.Messages.Parse.fst

@@ -24,11 +24,11 @@ let emp_inames_disjoint (t:inames)
 ```pulse
 ghost
 fn elim_implies (#p #q:vprop) ()
-   requires `@(p @==> q) ** p
+   requires (p @==> q) ** p
    ensures q
 {
   open Pulse.Lib.Stick;
-  rewrite `@(p @==> q) as (stick #emp_inames p q);
+  rewrite (p @==> q) as (stick #emp_inames p q);
   elim_stick #emp_inames p q;
 }
 ```
@@ -283,8 +283,8 @@ fn parse_dpe_cmd (#s:erased (Seq.seq U8.t))
                 dpe_cmd_args = cmd_args;
               };
 *)              
-              rewrite (raw_data_item_match full_perm cmd_args vargs ** `@(raw_data_item_match full_perm cmd_args vargs @==> A.pts_to input #p s)) // FIXME: should `fold` honor projectors and not just `match`?
-                as (raw_data_item_match full_perm res.dpe_cmd_args vargs ** `@(raw_data_item_match full_perm res.dpe_cmd_args vargs @==> A.pts_to input #p s));
+              rewrite (raw_data_item_match full_perm cmd_args vargs ** (raw_data_item_match full_perm cmd_args vargs @==> A.pts_to input #p s)) // FIXME: should `fold` honor projectors and not just `match`?
+                as (raw_data_item_match full_perm res.dpe_cmd_args vargs ** (raw_data_item_match full_perm res.dpe_cmd_args vargs @==> A.pts_to input #p s));
               fold (parse_dpe_cmd_post len input s p (Some res));
               Some res
             }

share/steel/examples/pulse/dice/dpe/DPE_CBOR.fst

@@ -31,11 +31,11 @@ let emp_inames_disjoint (t:inames)
 ```pulse
 ghost
 fn elim_implies () (#p #q:vprop)
-   requires `@(p @==> q) ** p
+   requires (p @==> q) ** p
    ensures q
 {
   open Pulse.Lib.Stick;
-  rewrite `@(p @==> q) as (stick #emp_inames p q);
+  rewrite (p @==> q) as (stick #emp_inames p q);
   elim_stick #emp_inames p q;
 }
 ```
@@ -46,7 +46,7 @@ fn finish (c:cbor_read_t)
           (#v:erased (raw_data_item))
           (#s:erased (Seq.seq U8.t))
           (#rem:erased (Seq.seq U8.t))
-  requires `@((raw_data_item_match full_perm c.cbor_read_payload v **
+  requires ((raw_data_item_match full_perm c.cbor_read_payload v **
                A.pts_to c.cbor_read_remainder #p rem) @==>
               A.pts_to input #p s) **
             raw_data_item_match full_perm c.cbor_read_payload v **

share/steel/examples/pulse/lib/Pulse.Lib.FlippableInv.fst

@@ -24,7 +24,7 @@ fn __mk_finv (p:vprop)
    let r = GR.alloc false;
    GR.share2 r;
    rewrite emp
-        as `@(if false then p else emp);
+        as (if false then p else emp);
    fold finv_p p r;
    let i = new_invariant' (finv_p p r);
    let fi = Mkfinv r i; // See #121
@@ -52,7 +52,7 @@ fn __flip_on (#p:vprop) (fi : finv p)
 
     GR.gather2 fi.r;
 
-    rewrite `@(if false then p else emp)
+    rewrite (if false then p else emp)
          as emp;
 
     fi.r := true;
@@ -85,7 +85,7 @@ fn __flip_off (#p:vprop) (fi : finv p)
     GR.share2 fi.r;
 
     rewrite emp
-         as `@(if false then p else emp);
+         as (if false then p else emp);
 
     fold finv_p p fi.r;
     fold (off fi)

share/steel/examples/pulse/lib/Pulse.Lib.Par.Pledge.fst

@@ -212,20 +212,20 @@ fn __elim_l (#os0:inames) (#f:vprop) (v1:vprop) (v2:vprop) (r1 r2 : GR.ref bool)
       by the other subpledge, so we just extract our resource. *)
       assert (pts_to r1 false);
       r1 := true;
-      rewrite emp ** `@(match false, true with
+      rewrite emp ** (match false, true with
                  | false, false -> pledge os0 f (v1 ** v2)
                  | false, true -> v1
                  | true, false -> v2
                  | true, true -> emp)
-           as `@(match true, true with
+           as (match true, true with
                  | false, false -> pledge os0 f (v1 ** v2)
                  | false, true -> v1
                  | true, false -> v2
                  | true, true -> emp) ** v1;
 
       (* I don't understand why this remains in the ctx, but get rid
       of it as it's just emp *)
-      rewrite `@(match true, true with
+      rewrite (match true, true with
                  | false, false -> pledge os0 f (v1 ** v2)
                  | false, true -> v1
                  | true, false -> v2
@@ -243,7 +243,7 @@ fn __elim_l (#os0:inames) (#f:vprop) (v1:vprop) (v2:vprop) (r1 r2 : GR.ref bool)
       Claim it, split it, and store the leftover in the invariant. *)
       assert (pts_to r1 false);
 
-      rewrite `@(match false, false with
+      rewrite (match false, false with
                  | false, false -> pledge os0 f (v1 ** v2)
                  | false, true -> v1
                  | true, false -> v2
@@ -257,7 +257,7 @@ fn __elim_l (#os0:inames) (#f:vprop) (v1:vprop) (v2:vprop) (r1 r2 : GR.ref bool)
       r1 := true;
 
       rewrite v2
-           as `@(match true, false with
+           as (match true, false with
                  | false, false -> pledge os0 f (v1 ** v2)
                  | false, true -> v1
                  | true, false -> v2
@@ -304,7 +304,7 @@ fn __split_pledge (#os:inames) (#f:vprop) (v1:vprop) (v2:vprop)
    GR.share2 r2;
 
    rewrite (pledge os f (v1 ** v2))
-        as `@(match false, false with
+        as (match false, false with
             | false, false -> pledge os f (v1 ** v2)
             | false, true -> v1
             | true, false -> v2
@@ -313,7 +313,7 @@ fn __split_pledge (#os:inames) (#f:vprop) (v1:vprop) (v2:vprop)
   assert (
      GR.pts_to r1 #one_half false
   ** GR.pts_to r2 #one_half false
-  ** `@(match false, false with
+  ** (match false, false with
       | false, false -> pledge os f (v1 ** v2)
       | false, true -> v1
       | true, false -> v2