diff options
Diffstat (limited to 'tests/fstar/arrays')
| -rw-r--r-- | tests/fstar/arrays/Arrays.Funs.fst | 27 |
1 files changed, 11 insertions, 16 deletions
diff --git a/tests/fstar/arrays/Arrays.Funs.fst b/tests/fstar/arrays/Arrays.Funs.fst index cf0f4f8b..731c7290 100644 --- a/tests/fstar/arrays/Arrays.Funs.fst +++ b/tests/fstar/arrays/Arrays.Funs.fst @@ -23,23 +23,22 @@ let array_to_mut_slice_ (t : Type0) (s : array t 32) : result ((slice t) & (slice t -> result (array t 32))) = - let* (s1, to_slice_mut_back) = array_to_slice_mut t 32 s in - Return (s1, to_slice_mut_back) + array_to_slice_mut t 32 s (** [arrays::array_len]: Source: 'src/arrays.rs', lines 25:0-25:40 *) let array_len (t : Type0) (s : array t 32) : result usize = - let* s1 = array_to_slice t 32 s in let i = slice_len t s1 in Return i + let* s1 = array_to_slice t 32 s in Return (slice_len t s1) (** [arrays::shared_array_len]: Source: 'src/arrays.rs', lines 29:0-29:48 *) let shared_array_len (t : Type0) (s : array t 32) : result usize = - let* s1 = array_to_slice t 32 s in let i = slice_len t s1 in Return i + let* s1 = array_to_slice t 32 s in Return (slice_len t s1) (** [arrays::shared_slice_len]: Source: 'src/arrays.rs', lines 33:0-33:44 *) let shared_slice_len (t : Type0) (s : slice t) : result usize = - let i = slice_len t s in Return i + Return (slice_len t s) (** [arrays::index_array_shared]: Source: 'src/arrays.rs', lines 37:0-37:57 *) @@ -62,8 +61,7 @@ let index_mut_array (t : Type0) (s : array t 32) (i : usize) : result (t & (t -> result (array t 32))) = - let* (x, index_mut_back) = array_index_mut_usize t 32 s i in - Return (x, index_mut_back) + array_index_mut_usize t 32 s i (** [arrays::index_slice]: Source: 'src/arrays.rs', lines 56:0-56:46 *) @@ -76,8 +74,7 @@ let index_mut_slice (t : Type0) (s : slice t) (i : usize) : result (t & (t -> result (slice t))) = - let* (x, index_mut_back) = slice_index_mut_usize t s i in - Return (x, index_mut_back) + slice_index_mut_usize t s i (** [arrays::slice_subslice_shared_]: Source: 'src/arrays.rs', lines 64:0-64:70 *) @@ -110,8 +107,7 @@ let array_to_slice_mut_ (x : array u32 32) : result ((slice u32) & (slice u32 -> result (array u32 32))) = - let* (s, to_slice_mut_back) = array_to_slice_mut u32 32 x in - Return (s, to_slice_mut_back) + array_to_slice_mut u32 32 x (** [arrays::array_subslice_shared_]: Source: 'src/arrays.rs', lines 80:0-80:74 *) @@ -272,8 +268,8 @@ let update_mut_slice (x : slice u32) : result (slice u32) = let update_all : result unit = let* _ = update_array (mk_array u32 2 [ 0; 0 ]) in let* _ = update_array (mk_array u32 2 [ 0; 0 ]) in - let* a = update_array_mut_borrow (mk_array u32 2 [ 0; 0 ]) in - let* (s, to_slice_mut_back) = array_to_slice_mut u32 2 a in + let* x = update_array_mut_borrow (mk_array u32 2 [ 0; 0 ]) in + let* (s, to_slice_mut_back) = array_to_slice_mut u32 2 x in let* s1 = update_mut_slice s in let* _ = to_slice_mut_back s1 in Return () @@ -308,7 +304,7 @@ let take_array_t (a : array aB_t 2) : result unit = (** [arrays::non_copyable_array]: Source: 'src/arrays.rs', lines 229:0-229:27 *) let non_copyable_array : result unit = - let* _ = take_array_t (mk_array aB_t 2 [ AB_A; AB_B ]) in Return () + take_array_t (mk_array aB_t 2 [ AB_A; AB_B ]) (** [arrays::sum]: loop 0: Source: 'src/arrays.rs', lines 242:0-250:1 *) @@ -444,8 +440,7 @@ let rec iter_mut_slice_loop Tot (result unit) (decreases (iter_mut_slice_loop_decreases len i)) = if i < len - then - let* i1 = usize_add i 1 in let* _ = iter_mut_slice_loop len i1 in Return () + then let* i1 = usize_add i 1 in iter_mut_slice_loop len i1 else Return () (** [arrays::iter_mut_slice]: |