clarify comments in exercise_03

verus-lang · Nov 2, 2024 · ac72105 · ac72105
1 parent 973069a
commit ac72105
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/2024-sosp-tutorial/exercises/advanced-rust-topics/exercise_03_counting_to_2.rs b/2024-sosp-tutorial/exercises/advanced-rust-topics/exercise_03_counting_to_2.rs
@@ -137,17 +137,17 @@ tokenized_state_machine!(
 
         #[inductive(tr_inc_a)]
         fn tr_inc_a_preserves_the_invariant(pre: Self, post: Self) {
-            /* proof here */
+            /* You can leave this empty */
         }
 
         #[inductive(tr_inc_b)]
         fn tr_inc_b_preserves_the_invariant(pre: Self, post: Self) {
-            /* proof here */
+            /* You can leave this empty */
         }
 
         #[inductive(initialize)]
         fn initial_state_satisfies_inv(post: Self) {
-            /* proof here */
+            /* You can leave this empty */
         }
     }
 );