diff options
Diffstat (limited to 'tests/coq/arrays')
-rw-r--r-- | tests/coq/arrays/Arrays.v | 21 |
1 files changed, 6 insertions, 15 deletions
diff --git a/tests/coq/arrays/Arrays.v b/tests/coq/arrays/Arrays.v index 34d163b7..580e72f0 100644 --- a/tests/coq/arrays/Arrays.v +++ b/tests/coq/arrays/Arrays.v @@ -30,9 +30,7 @@ Definition array_to_mut_slice_ (T : Type) (s : array T 32%usize) : result ((slice T) * (slice T -> result (array T 32%usize))) := - p <- array_to_slice_mut T 32%usize s; - let (s1, to_slice_mut_back) := p in - Return (s1, to_slice_mut_back) + array_to_slice_mut T 32%usize s . (** [arrays::array_len]: @@ -78,9 +76,7 @@ Definition index_mut_array (T : Type) (s : array T 32%usize) (i : usize) : result (T * (T -> result (array T 32%usize))) := - p <- array_index_mut_usize T 32%usize s i; - let (t, index_mut_back) := p in - Return (t, index_mut_back) + array_index_mut_usize T 32%usize s i . (** [arrays::index_slice]: @@ -95,9 +91,7 @@ Definition index_mut_slice (T : Type) (s : slice T) (i : usize) : result (T * (T -> result (slice T))) := - p <- slice_index_mut_usize T s i; - let (t, index_mut_back) := p in - Return (t, index_mut_back) + slice_index_mut_usize T s i . (** [arrays::slice_subslice_shared_]: @@ -136,9 +130,7 @@ Definition array_to_slice_mut_ (x : array u32 32%usize) : result ((slice u32) * (slice u32 -> result (array u32 32%usize))) := - p <- array_to_slice_mut u32 32%usize x; - let (s, to_slice_mut_back) := p in - Return (s, to_slice_mut_back) + array_to_slice_mut u32 32%usize x . (** [arrays::array_subslice_shared_]: @@ -381,7 +373,7 @@ Definition take_array_t (a : array AB_t 2%usize) : result unit := (** [arrays::non_copyable_array]: Source: 'src/arrays.rs', lines 229:0-229:27 *) Definition non_copyable_array : result unit := - _ <- take_array_t (mk_array AB_t 2%usize [ AB_A; AB_B ]); Return tt + take_array_t (mk_array AB_t 2%usize [ AB_A; AB_B ]) . (** [arrays::sum]: loop 0: @@ -548,8 +540,7 @@ Fixpoint iter_mut_slice_loop | O => Fail_ OutOfFuel | S n1 => if i s< len - then ( - i1 <- usize_add i 1%usize; _ <- iter_mut_slice_loop n1 len i1; Return tt) + then (i1 <- usize_add i 1%usize; iter_mut_slice_loop n1 len i1) else Return tt end . |