summaryrefslogtreecommitdiff
path: root/tests/fstar/array
diff options
context:
space:
mode:
Diffstat (limited to 'tests/fstar/array')
-rw-r--r--tests/fstar/array/Array.Funs.fst4
1 files changed, 4 insertions, 0 deletions
diff --git a/tests/fstar/array/Array.Funs.fst b/tests/fstar/array/Array.Funs.fst
index 7c1d0b09..72163585 100644
--- a/tests/fstar/array/Array.Funs.fst
+++ b/tests/fstar/array/Array.Funs.fst
@@ -139,6 +139,10 @@ let index_index_array_fwd
let* a = array_index_shared (array u32 32) 32 s i in
array_index_shared u32 32 a j
+(** [array::const_gen_ret]: forward function *)
+let const_gen_ret_fwd (n : usize) : result usize =
+ Return n
+
(** [array::update_update_array]: forward function *)
let update_update_array_fwd
(s : array (array u32 32) 32) (i : usize) (j : usize) : result unit =