fix examples

Author: tjhance

examples/atomic_increment.rs

@@ -58,7 +58,7 @@ pub fn increment_good(var: &PAtomicU64) -> (out: u64)
     ensures
         out == perm@.value,
 {
-    let Tracked(credit) = vstd::invariant::create_open_invariant_credit();
+    let tracked credit = vstd::invariant::create_open_invariant_credit();
     let tracked mut au = atomic_update;
 
     let mut curr;
@@ -70,7 +70,7 @@ pub fn increment_good(var: &PAtomicU64) -> (out: u64)
     proof { au = wrapped_au.get().tracked_unwrap_err() };
 
     loop invariant au == atomic_update {
-        let Tracked(credit) = vstd::invariant::create_open_invariant_credit();
+        let tracked credit = vstd::invariant::create_open_invariant_credit();
         let next = curr.wrapping_add(1);
 
         let res;
@@ -133,7 +133,7 @@ impl InvariantPredicate<int, PermissionU64> for UserInv {
 fn call_increment_good_inv() {
     let (var, Tracked(perm)) = PAtomicU64::new(6);
     let tracked inv = AtomicInvariant::<_, _, UserInv>::new(perm.id(), perm, USER_INV);
-    let Tracked(mut credit) = vstd::invariant::create_open_invariant_credit();
+    let tracked mut credit = vstd::invariant::create_open_invariant_credit();
 
     increment_good(&var) atomically loop |update| {
         let tracked mut spare = None;

examples/guide/logatom.rs

@@ -72,7 +72,7 @@ fn reset_client_async() {
     );
 
 // ANCHOR: reset_client_async
-let Tracked(mut credit) = vstd::invariant::create_open_invariant_credit();
+let tracked mut credit = vstd::invariant::create_open_invariant_credit();
 
 reset(&var) atomically |update| {
     open_atomic_invariant!(credit => &inv => perm => {
@@ -112,7 +112,7 @@ fn increment(var: &PAtomicU64) -> (out: u64)
         out == perm@.value,
 // ANCHOR_END: increment_signature_5
 {
-    let Tracked(credit) = vstd::invariant::create_open_invariant_credit();
+    let tracked credit = vstd::invariant::create_open_invariant_credit();
     let tracked mut au = atomic_update;
     let mut curr;
 
@@ -127,7 +127,7 @@ fn increment(var: &PAtomicU64) -> (out: u64)
 
     // compare exchange loop
     loop invariant au == atomic_update {
-        let Tracked(credit) = vstd::invariant::create_open_invariant_credit();
+        let tracked credit = vstd::invariant::create_open_invariant_credit();
         let next = curr.wrapping_add(1);
         let res;
 
@@ -186,7 +186,7 @@ fn increment_client_async() {
     );
 
 // ANCHOR: increment_client_async
-let Tracked(mut credit) = vstd::invariant::create_open_invariant_credit();
+let tracked mut credit = vstd::invariant::create_open_invariant_credit();
 
 increment(&var) atomically loop |update| {
     let tracked mut spare = None;

examples/helping.rs

@@ -429,7 +429,7 @@ fn main() {
         token.id(), token, USER_INV
     );
 
-    let Tracked(credit) = vstd::invariant::create_open_invariant_credit();
+    let tracked credit = vstd::invariant::create_open_invariant_credit();
     flag.flip() atomically |update| -> FlipAU {
         open_atomic_invariant!(credit => &inv => token => {
             let prev = token.value@;
@@ -438,7 +438,7 @@ fn main() {
         });
     };
 
-    let Tracked(credit) = vstd::invariant::create_open_invariant_credit();
+    let tracked credit = vstd::invariant::create_open_invariant_credit();
     let out = flag.read() atomically |update| -> ReadAU {
         open_atomic_invariant!(credit => &inv => token => {
             token = update(token).get();

examples/logatom_lib.rs

@@ -478,7 +478,7 @@ impl logatom::MutLinearizer<IncrementOp> for ClientInvCarrier<'_> {
 pub fn client_inv() {
     let (my_patomic, Tracked(my_perm)) = MyPAtomicU64::new(6, Ghost(1234));
     let tracked inv = AtomicInvariant::<_, _, UserInv>::new(my_perm.id(), my_perm, USER_INV);
-    let Tracked(mut credit) = vstd::invariant::create_open_invariant_credit();
+    let tracked mut credit = vstd::invariant::create_open_invariant_credit();
 
     let tracked carrier = ClientInvCarrier { my_inv: &inv, credit };
     let (prev, Tracked(_unit)) = increment::<ClientInvCarrier>(