Update the Makefile and regenerate the test files

1 files changed, 18 insertions, 23 deletions

diff --git a/tests/lean/Array/Funs.lean b/tests/lean/Array/Funs.lean
index b1365143..8a2c1045 100644
--- a/tests/lean/Array/Funs.lean
+++ b/tests/lean/Array/Funs.lean
@@ -9,24 +9,24 @@ namespace array
 /- [array::array_to_shared_slice_]: forward function -/
 def array_to_shared_slice_
   (T : Type) (s : Array T (Usize.ofInt 32)) : Result (Slice T) :=
-  Array.to_slice T (Usize.ofInt 32) s
+  Array.to_slice_shared T (Usize.ofInt 32) s
 
 /- [array::array_to_mut_slice_]: forward function -/
 def array_to_mut_slice_
   (T : Type) (s : Array T (Usize.ofInt 32)) : Result (Slice T) :=
-  Array.to_mut_slice T (Usize.ofInt 32) s
+  Array.to_slice_mut T (Usize.ofInt 32) s
 
 /- [array::array_to_mut_slice_]: backward function 0 -/
 def array_to_mut_slice__back
   (T : Type) (s : Array T (Usize.ofInt 32)) (ret0 : Slice T) :
   Result (Array T (Usize.ofInt 32))
   :=
-  Array.to_mut_slice_back T (Usize.ofInt 32) s ret0
+  Array.to_slice_mut_back T (Usize.ofInt 32) s ret0
 
 /- [array::array_len]: forward function -/
 def array_len (T : Type) (s : Array T (Usize.ofInt 32)) : Result Usize :=
   do
-    let s0 ← Array.to_slice T (Usize.ofInt 32) s
+    let s0 ← Array.to_slice_shared T (Usize.ofInt 32) s
     let i := Slice.len T s0
     Result.ret i
 
@@ -34,7 +34,7 @@ def array_len (T : Type) (s : Array T (Usize.ofInt 32)) : Result Usize :=
 def shared_array_len
   (T : Type) (s : Array T (Usize.ofInt 32)) : Result Usize :=
   do
-    let s0 ← Array.to_slice T (Usize.ofInt 32) s
+    let s0 ← Array.to_slice_shared T (Usize.ofInt 32) s
     let i := Slice.len T s0
     Result.ret i
 
@@ -109,21 +109,22 @@ def slice_subslice_mut__back
   :=
   Slice.subslice_mut_back U32 x (Range.mk y z) ret0
 
-/- [array::array_to_slice_shared]: forward function -/
-def array_to_slice_shared
+/- [array::array_to_slice_shared_]: forward function -/
+def array_to_slice_shared_
   (x : Array U32 (Usize.ofInt 32)) : Result (Slice U32) :=
-  Array.to_slice U32 (Usize.ofInt 32) x
+  Array.to_slice_shared U32 (Usize.ofInt 32) x
 
-/- [array::array_to_slice_mut]: forward function -/
-def array_to_slice_mut (x : Array U32 (Usize.ofInt 32)) : Result (Slice U32) :=
-  Array.to_mut_slice U32 (Usize.ofInt 32) x
+/- [array::array_to_slice_mut_]: forward function -/
+def array_to_slice_mut_
+  (x : Array U32 (Usize.ofInt 32)) : Result (Slice U32) :=
+  Array.to_slice_mut U32 (Usize.ofInt 32) x
 
-/- [array::array_to_slice_mut]: backward function 0 -/
-def array_to_slice_mut_back
+/- [array::array_to_slice_mut_]: backward function 0 -/
+def array_to_slice_mut__back
   (x : Array U32 (Usize.ofInt 32)) (ret0 : Slice U32) :
   Result (Array U32 (Usize.ofInt 32))
   :=
-  Array.to_mut_slice_back U32 (Usize.ofInt 32) x ret0
+  Array.to_slice_mut_back U32 (Usize.ofInt 32) x ret0
 
 /- [array::array_subslice_shared_]: forward function -/
 def array_subslice_shared_
@@ -186,17 +187,14 @@ def array_local_deep_copy (x : Array U32 (Usize.ofInt 32)) : Result Unit :=
 def f0 : Result Unit :=
   do
     let s ←
-      Array.to_mut_slice U32 (Usize.ofInt 2)
+      Array.to_slice_mut U32 (Usize.ofInt 2)
         (Array.make U32 (Usize.ofInt 2) [ (U32.ofInt 1), (U32.ofInt 2) ])
     let s0 ← Slice.index_mut_back U32 s (Usize.ofInt 0) (U32.ofInt 1)
     let _ ←
-      Array.to_mut_slice_back U32 (Usize.ofInt 2)
+      Array.to_slice_mut_back U32 (Usize.ofInt 2)
         (Array.make U32 (Usize.ofInt 2) [ (U32.ofInt 1), (U32.ofInt 2) ]) s0
     Result.ret ()
 
-/- Unit test for [array::f0] -/
-#assert (f0 == .ret ())
-
 /- [array::f1]: forward function -/
 def f1 : Result Unit :=
   do
@@ -206,9 +204,6 @@ def f1 : Result Unit :=
         (Usize.ofInt 0) (U32.ofInt 1)
     Result.ret ()
 
-/- Unit test for [array::f1] -/
-#assert (f1 == .ret ())
-
 /- [array::sum]: loop 0: forward function -/
 divergent def sum_loop (s : Slice U32) (sum0 : U32) (i : Usize) : Result U32 :=
   let i0 := Slice.len U32 s
@@ -268,7 +263,7 @@ def f3 : Result U32 :=
         (Usize.ofInt 0)
     let _ ← f2 i
     let s ←
-      Array.to_slice U32 (Usize.ofInt 2)
+      Array.to_slice_shared U32 (Usize.ofInt 2)
         (Array.make U32 (Usize.ofInt 2) [ (U32.ofInt 1), (U32.ofInt 2) ])
     let s0 ←
       f4