From 8543092569616ef6a75949a72532f7b73dc696f2 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 18 Aug 2023 12:23:03 +0200
Subject: Regenerate the array tests

---
 tests/lean/Array/Funs.lean | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'tests/lean')

diff --git a/tests/lean/Array/Funs.lean b/tests/lean/Array/Funs.lean
index 8d10c660..a42072d1 100644
--- a/tests/lean/Array/Funs.lean
+++ b/tests/lean/Array/Funs.lean
@@ -447,6 +447,14 @@ def f3 : Result U32 :=
           ]) (Usize.ofInt 16) (Usize.ofInt 18)
     sum2 s s0
 
+/- [array::SZ] -/
+def sz_body : Result Usize := Result.ret (Usize.ofInt 32)
+def sz_c : Usize := eval_global sz_body (by simp)
+
+/- [array::f5]: forward function -/
+def f5 (x : Array U32 (Usize.ofInt 32)) : Result U32 :=
+  Array.index_shared U32 (Usize.ofInt 32) x (Usize.ofInt 0)
+
 /- [array::ite]: forward function -/
 def ite : Result Unit :=
   do
-- 
cgit v1.2.3