From f3e16bb43a8ff27a5184d9fa452277cc6a59410f Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 19 Mar 2024 05:29:29 +0100
Subject: Regenerate the tests

---
 tests/lean/Arrays.lean | 28 ++++++++--------------------
 1 file changed, 8 insertions(+), 20 deletions(-)

(limited to 'tests/lean/Arrays.lean')

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]:
-- 
cgit v1.2.3


From 5e99d127e0a746f5779779756fccf79f15c19d10 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 20 Mar 2024 06:17:41 +0100
Subject: Regenerate the code

---
 tests/lean/Arrays.lean | 13 +++++--------
 1 file changed, 5 insertions(+), 8 deletions(-)

(limited to 'tests/lean/Arrays.lean')

diff --git a/tests/lean/Arrays.lean b/tests/lean/Arrays.lean
index cd1b6544..207f31b9 100644
--- a/tests/lean/Arrays.lean
+++ b/tests/lean/Arrays.lean
@@ -35,22 +35,19 @@ def array_to_mut_slice_
 def array_len (T : Type) (s : Array T 32#usize) : Result Usize :=
   do
   let s1 ← Array.to_slice T 32#usize s
-  let i := Slice.len T s1
-  Result.ret i
+  Result.ret (Slice.len T s1)
 
 /- [arrays::shared_array_len]:
    Source: 'src/arrays.rs', lines 29:0-29:48 -/
 def shared_array_len (T : Type) (s : Array T 32#usize) : Result Usize :=
   do
   let s1 ← Array.to_slice T 32#usize s
-  let i := Slice.len T s1
-  Result.ret i
+  Result.ret (Slice.len T s1)
 
 /- [arrays::shared_slice_len]:
    Source: 'src/arrays.rs', lines 33:0-33:44 -/
 def shared_slice_len (T : Type) (s : Slice T) : Result Usize :=
-  let i := Slice.len T s
-  Result.ret i
+  Result.ret (Slice.len T s)
 
 /- [arrays::index_array_shared]:
    Source: 'src/arrays.rs', lines 37:0-37:57 -/
@@ -305,8 +302,8 @@ def update_all : Result Unit :=
   do
   let _ ← update_array (Array.make U32 2#usize [ 0#u32, 0#u32 ])
   let _ ← update_array (Array.make U32 2#usize [ 0#u32, 0#u32 ])
-  let a ← update_array_mut_borrow (Array.make U32 2#usize [ 0#u32, 0#u32 ])
-  let (s, to_slice_mut_back) ← Array.to_slice_mut U32 2#usize a
+  let x ← update_array_mut_borrow (Array.make U32 2#usize [ 0#u32, 0#u32 ])
+  let (s, to_slice_mut_back) ← Array.to_slice_mut U32 2#usize x
   let s1 ← update_mut_slice s
   let _ ← to_slice_mut_back s1
   Result.ret ()
-- 
cgit v1.2.3