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/coq/array/Array_Funs.v | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'tests/coq')

diff --git a/tests/coq/array/Array_Funs.v b/tests/coq/array/Array_Funs.v
index d47e4633..6ff3066a 100644
--- a/tests/coq/array/Array_Funs.v
+++ b/tests/coq/array/Array_Funs.v
@@ -451,6 +451,15 @@ Definition f3_fwd (n : nat) : result u32 :=
   sum2_fwd n s s0
 .
 
+(** [array::SZ] *)
+Definition sz_body : result usize := Return 32%usize.
+Definition sz_c : usize := sz_body%global.
+
+(** [array::f5]: forward function *)
+Definition f5_fwd (x : array u32 32%usize) : result u32 :=
+  array_index_shared u32 32%usize x 0%usize
+.
+
 (** [array::ite]: forward function *)
 Definition ite_fwd : result unit :=
   s <-
-- 
cgit v1.2.3