diff options
Diffstat (limited to 'tests/fstar/array')
| -rw-r--r-- | tests/fstar/array/Array.Funs.fst | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/tests/fstar/array/Array.Funs.fst b/tests/fstar/array/Array.Funs.fst index 72163585..83256398 100644 --- a/tests/fstar/array/Array.Funs.fst +++ b/tests/fstar/array/Array.Funs.fst @@ -347,6 +347,14 @@ let f3_fwd : result u32 = ]) 16 18 in sum2_fwd s s0 +(** [array::SZ] *) +let sz_body : result usize = Return 32 +let sz_c : usize = eval_global sz_body + +(** [array::f5]: forward function *) +let f5_fwd (x : array u32 32) : result u32 = + array_index_shared u32 32 x 0 + (** [array::ite]: forward function *) let ite_fwd : result unit = let* s = array_to_slice_mut_fwd u32 2 (mk_array u32 2 [ 0; 0 ]) in |