diff options
Diffstat (limited to 'tests/fstar/array/Array.Funs.fst')
| -rw-r--r-- | tests/fstar/array/Array.Funs.fst | 4 |
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 = |