From f74647773d7dd21580fd938dd9b4e300719b0234 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 8 Mar 2024 08:03:48 +0100
Subject: Regenerate the test files

---
 tests/lean/Arrays.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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

diff --git a/tests/lean/Arrays.lean b/tests/lean/Arrays.lean
index 5158ca28..6f9cd94c 100644
--- a/tests/lean/Arrays.lean
+++ b/tests/lean/Arrays.lean
@@ -397,7 +397,7 @@ divergent def sum2_loop
 def sum2 (s : Slice U32) (s2 : Slice U32) : Result U32 :=
   let i := Slice.len U32 s
   let i1 := Slice.len U32 s2
-  if not (i = i1)
+  if ¬ (i = i1)
   then Result.fail .panic
   else sum2_loop s s2 0#u32 0#usize
 
-- 
cgit v1.2.3


From 44248ccfe3bfb8c45e5bb434d8dfb3dfa6e6b69c Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 8 Mar 2024 09:42:29 +0100
Subject: Update the generation of constant bodies for Lean

---
 tests/lean/Arrays.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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

diff --git a/tests/lean/Arrays.lean b/tests/lean/Arrays.lean
index 6f9cd94c..d2bb7cf2 100644
--- a/tests/lean/Arrays.lean
+++ b/tests/lean/Arrays.lean
@@ -452,7 +452,7 @@ def f3 : Result U32 :=
 /- [arrays::SZ]
    Source: 'src/arrays.rs', lines 286:0-286:19 -/
 def sz_body : Result Usize := Result.ret 32#usize
-def sz_c : Usize := eval_global sz_body (by decide)
+def sz_c : Usize := eval_global sz_body
 
 /- [arrays::f5]:
    Source: 'src/arrays.rs', lines 289:0-289:31 -/
-- 
cgit v1.2.3