Regenerate the tests

6 files changed, 30 insertions, 73 deletions

diff --git a/tests/lean/Arrays.lean b/tests/lean/Arrays.lean
index d637ee13..cd1b6544 100644
--- a/tests/lean/Arrays.lean
+++ b/tests/lean/Arrays.lean
@@ -28,9 +28,7 @@ def array_to_mut_slice_
   (T : Type) (s : Array T 32#usize) :
   Result ((Slice T) × (Slice T → Result (Array T 32#usize)))
   :=
-  do
-  let (s1, to_slice_mut_back) ← Array.to_slice_mut T 32#usize s
-  Result.ret (s1, to_slice_mut_back)
+  Array.to_slice_mut T 32#usize s
 
 /- [arrays::array_len]:
    Source: 'src/arrays.rs', lines 25:0-25:40 -/
@@ -76,9 +74,7 @@ def index_mut_array
   (T : Type) (s : Array T 32#usize) (i : Usize) :
   Result (T × (T → Result (Array T 32#usize)))
   :=
-  do
-  let (t, index_mut_back) ← Array.index_mut_usize T 32#usize s i
-  Result.ret (t, index_mut_back)
+  Array.index_mut_usize T 32#usize s i
 
 /- [arrays::index_slice]:
    Source: 'src/arrays.rs', lines 56:0-56:46 -/
@@ -91,9 +87,7 @@ def index_mut_slice
   (T : Type) (s : Slice T) (i : Usize) :
   Result (T × (T → Result (Slice T)))
   :=
-  do
-  let (t, index_mut_back) ← Slice.index_mut_usize T s i
-  Result.ret (t, index_mut_back)
+  Slice.index_mut_usize T s i
 
 /- [arrays::slice_subslice_shared_]:
    Source: 'src/arrays.rs', lines 64:0-64:70 -/
@@ -127,9 +121,7 @@ def array_to_slice_mut_
   (x : Array U32 32#usize) :
   Result ((Slice U32) × (Slice U32 → Result (Array U32 32#usize)))
   :=
-  do
-  let (s, to_slice_mut_back) ← Array.to_slice_mut U32 32#usize x
-  Result.ret (s, to_slice_mut_back)
+  Array.to_slice_mut U32 32#usize x
 
 /- [arrays::array_subslice_shared_]:
    Source: 'src/arrays.rs', lines 80:0-80:74 -/
@@ -354,9 +346,7 @@ def take_array_t (a : Array AB 2#usize) : Result Unit :=
 /- [arrays::non_copyable_array]:
    Source: 'src/arrays.rs', lines 229:0-229:27 -/
 def non_copyable_array : Result Unit :=
-  do
-  let _ ← take_array_t (Array.make AB 2#usize [ AB.A, AB.B ])
-  Result.ret ()
+  take_array_t (Array.make AB 2#usize [ AB.A, AB.B ])
 
 /- [arrays::sum]: loop 0:
    Source: 'src/arrays.rs', lines 242:0-250:1 -/
@@ -496,11 +486,9 @@ def zero_slice (a : Slice U8) : Result (Slice U8) :=
    Source: 'src/arrays.rs', lines 312:0-318:1 -/
 divergent def iter_mut_slice_loop (len : Usize) (i : Usize) : Result Unit :=
   if i < len
-  then
-    do
-    let i1 ← i + 1#usize
-    let _ ← iter_mut_slice_loop len i1
-    Result.ret ()
+  then do
+       let i1 ← i + 1#usize
+       iter_mut_slice_loop len i1
   else Result.ret ()
 
 /- [arrays::iter_mut_slice]:
diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/BetreeMain/Funs.lean
index d6449b37..bd5921a8 100644
--- a/tests/lean/BetreeMain/Funs.lean
+++ b/tests/lean/BetreeMain/Funs.lean
@@ -21,9 +21,7 @@ def betree.store_internal_node
   (id : U64) (content : betree.List (U64 × betree.Message)) (st : State) :
   Result (State × Unit)
   :=
-  do
-  let (st1, _) ← betree_utils.store_internal_node id content st
-  Result.ret (st1, ())
+  betree_utils.store_internal_node id content st
 
 /- [betree_main::betree::load_leaf_node]:
    Source: 'src/betree.rs', lines 46:0-46:44 -/
@@ -37,9 +35,7 @@ def betree.store_leaf_node
   (id : U64) (content : betree.List (U64 × U64)) (st : State) :
   Result (State × Unit)
   :=
-  do
-  let (st1, _) ← betree_utils.store_leaf_node id content st
-  Result.ret (st1, ())
+  betree_utils.store_leaf_node id content st
 
 /- [betree_main::betree::fresh_node_id]:
    Source: 'src/betree.rs', lines 55:0-55:48 -/
diff --git a/tests/lean/Demo/Demo.lean b/tests/lean/Demo/Demo.lean
index f38b5cd3..09032820 100644
--- a/tests/lean/Demo/Demo.lean
+++ b/tests/lean/Demo/Demo.lean
@@ -116,9 +116,7 @@ def list_nth_mut1
   (T : Type) (l : CList T) (i : U32) :
   Result (T × (T → Result (CList T)))
   :=
-  do
-  let (t, back_'a) ← list_nth_mut1_loop T l i
-  Result.ret (t, back_'a)
+  list_nth_mut1_loop T l i
 
 /- [demo::i32_id]:
    Source: 'src/demo.rs', lines 80:0-80:28 -/
diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean
index f0706725..d33b6571 100644
--- a/tests/lean/Hashmap/Funs.lean
+++ b/tests/lean/Hashmap/Funs.lean
@@ -311,9 +311,7 @@ def HashMap.get_mut_in_list
   (T : Type) (ls : List T) (key : Usize) :
   Result (T × (T → Result (List T)))
   :=
-  do
-  let (t, back_'a) ← HashMap.get_mut_in_list_loop T ls key
-  Result.ret (t, back_'a)
+  HashMap.get_mut_in_list_loop T ls key
 
 /- [hashmap::{hashmap::HashMap<T>}::get_mut]:
    Source: 'src/hashmap.rs', lines 257:4-257:67 -/
diff --git a/tests/lean/HashmapMain/Funs.lean b/tests/lean/HashmapMain/Funs.lean
index 31441b4a..8a277700 100644
--- a/tests/lean/HashmapMain/Funs.lean
+++ b/tests/lean/HashmapMain/Funs.lean
@@ -326,9 +326,7 @@ def hashmap.HashMap.get_mut_in_list
   (T : Type) (ls : hashmap.List T) (key : Usize) :
   Result (T × (T → Result (hashmap.List T)))
   :=
-  do
-  let (t, back_'a) ← hashmap.HashMap.get_mut_in_list_loop T ls key
-  Result.ret (t, back_'a)
+  hashmap.HashMap.get_mut_in_list_loop T ls key
 
 /- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut]:
    Source: 'src/hashmap.rs', lines 257:4-257:67 -/
@@ -460,8 +458,7 @@ def insert_on_disk
   do
   let (st1, hm) ← hashmap_utils.deserialize st
   let hm1 ← hashmap.HashMap.insert U64 hm key value
-  let (st2, _) ← hashmap_utils.serialize hm1 st1
-  Result.ret (st2, ())
+  hashmap_utils.serialize hm1 st1
 
 /- [hashmap_main::main]:
    Source: 'src/hashmap_main.rs', lines 16:0-16:13 -/
diff --git a/tests/lean/Loops.lean b/tests/lean/Loops.lean
index 433ca8f0..3f075347 100644
--- a/tests/lean/Loops.lean
+++ b/tests/lean/Loops.lean
@@ -138,9 +138,7 @@ divergent def list_nth_mut_loop_loop
    Source: 'src/loops.rs', lines 88:0-88:71 -/
 def list_nth_mut_loop
   (T : Type) (ls : List T) (i : U32) : Result (T × (T → Result (List T))) :=
-  do
-  let (t, back) ← list_nth_mut_loop_loop T ls i
-  Result.ret (t, back)
+  list_nth_mut_loop_loop T ls i
 
 /- [loops::list_nth_shared_loop]: loop 0:
    Source: 'src/loops.rs', lines 101:0-111:1 -/
@@ -322,9 +320,7 @@ def list_nth_mut_loop_pair
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
   Result ((T × T) × (T → Result (List T)) × (T → Result (List T)))
   :=
-  do
-  let (p, back_'a, back_'b) ← list_nth_mut_loop_pair_loop T ls0 ls1 i
-  Result.ret (p, back_'a, back_'b)
+  list_nth_mut_loop_pair_loop T ls0 ls1 i
 
 /- [loops::list_nth_shared_loop_pair]: loop 0:
    Source: 'src/loops.rs', lines 208:0-229:1 -/
@@ -384,9 +380,7 @@ def list_nth_mut_loop_pair_merge
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
   Result ((T × T) × ((T × T) → Result ((List T) × (List T))))
   :=
-  do
-  let (p, back_'a) ← list_nth_mut_loop_pair_merge_loop T ls0 ls1 i
-  Result.ret (p, back_'a)
+  list_nth_mut_loop_pair_merge_loop T ls0 ls1 i
 
 /- [loops::list_nth_shared_loop_pair_merge]: loop 0:
    Source: 'src/loops.rs', lines 251:0-266:1 -/
@@ -443,9 +437,7 @@ def list_nth_mut_shared_loop_pair
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
   Result ((T × T) × (T → Result (List T)))
   :=
-  do
-  let (p, back_'a) ← list_nth_mut_shared_loop_pair_loop T ls0 ls1 i
-  Result.ret (p, back_'a)
+  list_nth_mut_shared_loop_pair_loop T ls0 ls1 i
 
 /- [loops::list_nth_mut_shared_loop_pair_merge]: loop 0:
    Source: 'src/loops.rs', lines 288:0-303:1 -/
@@ -480,9 +472,7 @@ def list_nth_mut_shared_loop_pair_merge
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
   Result ((T × T) × (T → Result (List T)))
   :=
-  do
-  let (p, back_'a) ← list_nth_mut_shared_loop_pair_merge_loop T ls0 ls1 i
-  Result.ret (p, back_'a)
+  list_nth_mut_shared_loop_pair_merge_loop T ls0 ls1 i
 
 /- [loops::list_nth_shared_mut_loop_pair]: loop 0:
    Source: 'src/loops.rs', lines 307:0-322:1 -/
@@ -516,9 +506,7 @@ def list_nth_shared_mut_loop_pair
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
   Result ((T × T) × (T → Result (List T)))
   :=
-  do
-  let (p, back_'b) ← list_nth_shared_mut_loop_pair_loop T ls0 ls1 i
-  Result.ret (p, back_'b)
+  list_nth_shared_mut_loop_pair_loop T ls0 ls1 i
 
 /- [loops::list_nth_shared_mut_loop_pair_merge]: loop 0:
    Source: 'src/loops.rs', lines 326:0-341:1 -/
@@ -553,19 +541,15 @@ def list_nth_shared_mut_loop_pair_merge
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
   Result ((T × T) × (T → Result (List T)))
   :=
-  do
-  let (p, back_'a) ← list_nth_shared_mut_loop_pair_merge_loop T ls0 ls1 i
-  Result.ret (p, back_'a)
+  list_nth_shared_mut_loop_pair_merge_loop T ls0 ls1 i
 
 /- [loops::ignore_input_mut_borrow]: loop 0:
    Source: 'src/loops.rs', lines 345:0-349:1 -/
 divergent def ignore_input_mut_borrow_loop (i : U32) : Result Unit :=
   if i > 0#u32
-  then
-    do
-    let i1 ← i - 1#u32
-    let _ ← ignore_input_mut_borrow_loop i1
-    Result.ret ()
+  then do
+       let i1 ← i - 1#u32
+       ignore_input_mut_borrow_loop i1
   else Result.ret ()
 
 /- [loops::ignore_input_mut_borrow]:
@@ -579,11 +563,9 @@ def ignore_input_mut_borrow (_a : U32) (i : U32) : Result U32 :=
    Source: 'src/loops.rs', lines 353:0-358:1 -/
 divergent def incr_ignore_input_mut_borrow_loop (i : U32) : Result Unit :=
   if i > 0#u32
-  then
-    do
-    let i1 ← i - 1#u32
-    let _ ← incr_ignore_input_mut_borrow_loop i1
-    Result.ret ()
+  then do
+       let i1 ← i - 1#u32
+       incr_ignore_input_mut_borrow_loop i1
   else Result.ret ()
 
 /- [loops::incr_ignore_input_mut_borrow]:
@@ -598,11 +580,9 @@ def incr_ignore_input_mut_borrow (a : U32) (i : U32) : Result U32 :=
    Source: 'src/loops.rs', lines 362:0-366:1 -/
 divergent def ignore_input_shared_borrow_loop (i : U32) : Result Unit :=
   if i > 0#u32
-  then
-    do
-    let i1 ← i - 1#u32
-    let _ ← ignore_input_shared_borrow_loop i1
-    Result.ret ()
+  then do
+       let i1 ← i - 1#u32
+       ignore_input_shared_borrow_loop i1
   else Result.ret ()
 
 /- [loops::ignore_input_shared_borrow]: